JordanChevalley

📁 Source: Mathlib/LinearAlgebra/JordanChevalley.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_isNilpotent_isSemisimple, exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow, isNilpotent_isSemisimple_unique	3
Total	3

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isNilpotent_isSemisimple 📖	mathematical	—	Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Subalgebra Semifield.toCommSemiring instSemiring instAlgebra smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet IsNilpotent LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow instMonoid IsSemisimple LinearMap.instAdd	—	smulCommClass_self IsScalarTower.left exists_squarefree_dvd_pow_of_ne_zero PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain minpoly.ne_zero_of_finite Module.Finite.linearMap Module.Free.of_divisionRing exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow PerfectField.separable_iff_squarefree
exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow 📖	mathematical	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing minpoly Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddCommGroup.toAddCommMonoid instRing instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Monoid.toNatPow Polynomial.semiring	Subalgebra instSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet IsNilpotent LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring instMonoid IsSemisimple LinearMap.instAdd	—	smulCommClass_self IsScalarTower.left Algebra.self_mem_adjoin_singleton AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass SubsemiringClass.toSubmonoidClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Polynomial.coe_aeval_mk_apply minpoly.aeval MulZeroClass.zero_mul IsCoprime.pow_left map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass minpoly.dvd_iff MulZeroClass.mul_zero zero_add map_one MonoidHomClass.toOneHomClass AlgHom.congr_arg IsUnit.of_mul_eq_one_right instIsDedekindFiniteMonoid Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero sub_mem SubringClass.addSubgroupClass Subalgebra.instSubringClass isSemisimple_of_squarefree_aeval_eq_zero Polynomial.Separable.squarefree sub_add_cancel
isNilpotent_isSemisimple_unique 📖	—	IsNilpotent Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow instMonoid Commute instMul LinearMap.instAdd	—	—	smulCommClass_self IsScalarTower.left exists_isNilpotent_isSemisimple Commute.add_right Commute.symm Commute.refl Commute.isNilpotent_sub Algebra.commute_of_mem_adjoin_singleton_of_commute IsSemisimple.sub_of_commute

---

← Back to Index