theorem
Diagonalization.isSemisimple_of_squarefree_charpoly
{K : Type u_1}
{V : Type u_2}
[Field K]
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
(f : Module.End K V)
(hsq : Squarefree (LinearMap.charpoly f))
:
theorem
Diagonalization.isSemisimple_of_charpoly_eq_prod_distinct
{K : Type u_1}
{V : Type u_2}
[Field K]
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
(f : Module.End K V)
{ι : Type u_3}
[Fintype ι]
(μ : ι → K)
(hμ : Function.Injective μ)
(hprod : LinearMap.charpoly f = ∏ i : ι, (Polynomial.X - Polynomial.C (μ i)))
:
def
Matrix.IsDiagonalizable
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{F : Type u_2}
[Field F]
(A : Matrix n n F)
: