Documentation Verification Report

Semisimple

📁 Source: Mathlib/LinearAlgebra/Semisimple.lean

Statistics

Metric	Count
Definitions `IsFinitelySemisimple`, `IsSemisimple`	2
Theorems `isSemisimple_iff`, `restrict`, `add_of_commute`, `aeval`, `isFinitelySemisimple`, `minpoly_squarefree`, `mul_of_commute`, `of_mem_adjoin_pair`, `of_mem_adjoin_singleton`, `pow`, `restrict`, `sub_of_commute`, `IsSemisimple_smul`, `IsSemisimple_smul_iff`, `eq_zero_of_isNilpotent_isSemisimple`, `eq_zero_of_isNilpotent_of_isFinitelySemisimple`, `isFinitelySemisimple_iff`, `isFinitelySemisimple_iff'`, `isFinitelySemisimple_iff_isSemisimple`, `isFinitelySemisimple_sub_algebraMap_iff`, `isSemisimple_id`, `isSemisimple_iff`, `isSemisimple_iff'`, `isSemisimple_neg`, `isSemisimple_of_squarefree_aeval_eq_zero`, `isSemisimple_restrict_iff`, `isSemisimple_sub_algebraMap_iff`, `isSemisimple_zero`	28
Total	30

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSemisimple_iff` 📖	mathematical	`LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `toLinearMap` `RingHomInvPair.ids`	`Module.End.IsSemisimple`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Module.AEval.instIsScalarTowerOrigPolynomial` `Module.AEval'.X_smul_of` `EquivLike.toEmbeddingLike` `LinearMap.congr_fun` `OrderIso.complementedLattice_iff` `RingHomSurjective.ids`

Module.End

Definitions

Name	Category	Theorems
`IsFinitelySemisimple` 📖	MathDef	7 math math: `LinearMap.IsSymmetric.isFinitelySemisimple`, `isFinitelySemisimple_sub_algebraMap_iff`, `IsFinitelySemisimple.restrict`, `isFinitelySemisimple_iff`, `isFinitelySemisimple_iff'`, `isFinitelySemisimple_iff_isSemisimple`, `IsSemisimple.isFinitelySemisimple`
`IsSemisimple` 📖	MathDef	25 math math: `isSemisimple_restrict_iff`, `isSemisimple_id`, `LieAlgebra.ad_isSemisimple_of_isSemisimple`, `IsSemisimple.mul_of_commute`, `IsSemisimple.add_of_commute`, `IsSemisimple.sub_of_commute`, `IsSemisimple.pow`, `IsSemisimple.restrict`, `isSemisimple_sub_algebraMap_iff`, `IsSemisimple.aeval`, `IsSemisimple.of_mem_adjoin_pair`, `IsSemisimple.of_mem_adjoin_singleton`, `isFinitelySemisimple_iff'`, `isSemisimple_neg`, `isSemisimple_zero`, `exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow`, `isSemisimple_of_squarefree_aeval_eq_zero`, `isFinitelySemisimple_iff_isSemisimple`, `IsSemisimple_smul`, `IsSemisimple_smul_iff`, `LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra`, `isSemisimple_iff'`, `LinearEquiv.isSemisimple_iff`, `exists_isNilpotent_isSemisimple`, `isSemisimple_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsSemisimple_smul` 📖	mathematical	—	`IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `IsSemisimple_smul_iff` `zero_smul` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule`
`IsSemisimple_smul_iff` 📖	mathematical	—	`IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `Submodule.comap_smul`
`eq_zero_of_isNilpotent_isSemisimple` 📖	mathematical	`IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `instMonoid`	`Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`smulCommClass_self` `IsScalarTower.left` `Polynomial.aeval_X` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.mem_ker` `apply_isScalarTower` `Module.AEval.annihilator_eq_ker_aeval` `apply_faithfulSMul` `IsSemisimpleModule.annihilator_isRadical` `Polynomial.aeval_X_pow`
`eq_zero_of_isNilpotent_of_isFinitelySemisimple` 📖	mathematical	`IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `instMonoid` `IsFinitelySemisimple`	`Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`isNilpotent.restrict` `eq_zero_of_isNilpotent_isSemisimple` `LinearMap.ext` `Submodule.subset_span` `lt_or_eq_of_le` `pow_apply` `Function.iterate_succ_apply'` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `instReflLe` `Set.ext` `Set.image_congr` `Module.Finite.span_of_finite` `Set.toFinite` `Finite.Set.finite_image` `Finite.of_fintype` `LinearMap.congr_fun`
`isFinitelySemisimple_iff` 📖	mathematical	—	`IsFinitelySemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtSubmodule` `Disjoint` `Submodule.instOrderBot` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—
`isFinitelySemisimple_iff'` 📖	mathematical	—	`IsFinitelySemisimple` `IsSemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `CommRing.toRing` `Submodule.module` `LinearMap.restrict`	—	—
`isFinitelySemisimple_iff_isSemisimple` 📖	mathematical	—	`IsFinitelySemisimple` `IsSemisimple`	—	`isSemisimple_iff` `isFinitelySemisimple_iff` `invtSubmodule.top_mem` `Module.Finite.top` `le_top` `codisjoint_iff` `IsSemisimple.isFinitelySemisimple`
`isFinitelySemisimple_sub_algebraMap_iff` 📖	mathematical	—	`IsFinitelySemisimple` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instSub` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `instSemiring` `RingHom.instFunLike` `algebraMap` `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`	—	`smulCommClass_self` `IsScalarTower.left` `sub_add_cancel` `Submodule.add_mem` `Submodule.smul_mem` `Submodule.sub_mem`
`isSemisimple_id` 📖	mathematical	—	`IsSemisimple` `LinearMap.id` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`invtSubmodule.id` `ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice`
`isSemisimple_iff` 📖	mathematical	—	`IsSemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtSubmodule` `IsCompl` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder`	—	—
`isSemisimple_iff'` 📖	mathematical	—	`IsSemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtSubmodule` `IsCompl` `Subtype.partialOrder` `Submodule.instPartialOrder` `invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice`	—	`IsSemisimple.eq_1` `isSemisimpleModule_iff` `smulCommClass_self` `IsScalarTower.left` `IsScalarTower.to_smulCommClass'` `apply_isScalarTower` `OrderIso.complementedLattice_iff` `complementedLattice_iff`
`isSemisimple_neg` 📖	mathematical	—	`IsSemisimple` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instNeg` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`Submodule.comap_neg`
`isSemisimple_of_squarefree_aeval_eq_zero` 📖	mathematical	`Squarefree` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Module.End` `AddCommGroup.toAddCommMonoid` `instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `AlgHom.funLike` `Polynomial.aeval` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring`	`IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`smulCommClass_self` `IsScalarTower.left` `Ideal.isRadical_iff_quotient_reduced` `isRadical_iff_span_singleton` `Squarefree.isRadical` `IsArtinianRing.instDecompositionMonoidPolynomial` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `FiniteDimensional.finiteDimensional_self` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsScalarTower.right` `PowerBasis.finite` `Squarefree.ne_zero` `Polynomial.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsArtinianRing.of_finite` `IsArtinianRing.isSemisimpleRing_of_isReduced` `Ideal.instIsTwoSided_1` `apply_isScalarTower` `Module.isTorsionBySet_iff_is_torsion_by_span` `Module.isTorsionBySet_singleton_iff` `Module.IsTorsionBy.eq_1` `Module.mem_annihilator` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Module.AEval.annihilator_eq_ker_aeval` `apply_faithfulSMul` `RingHom.mem_ker` `AddMonoidHom.map_add'` `LinearMap.isSemisimpleModule_iff_of_bijective` `Ideal.Quotient.instRingHomSurjectiveQuotientMk` `Function.bijective_id` `IsSemisimpleRing.isSemisimpleModule`
`isSemisimple_restrict_iff` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `invtSubmodule`	`IsSemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `CommRing.toRing` `Submodule.module` `LinearMap.restrict` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Sublattice.instSetLike` `invtSubmodule` `Disjoint` `Submodule.instOrderBot` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`smulCommClass_self` `IsScalarTower.left` `apply_isScalarTower` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `RingHomSurjective.ids` `RingHomInvPair.ids` `OrderIso.complementedLattice_iff` `Sublattice.infClosed` `Sublattice.supClosed`
`isSemisimple_sub_algebraMap_iff` 📖	mathematical	—	`IsSemisimple` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instSub` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `instSemiring` `RingHom.instFunLike` `algebraMap` `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`	—	`smulCommClass_self` `IsScalarTower.left` `sub_add_cancel` `Submodule.add_mem` `Submodule.smul_mem` `Submodule.sub_mem`
`isSemisimple_zero` 📖	mathematical	—	`IsSemisimple` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`invtSubmodule.zero` `ComplementedLattice.exists_isCompl` `IsSemisimpleModule.toComplementedLattice`

Module.End.IsFinitelySemisimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrict` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `Module.End.IsFinitelySemisimple`	`Module.End.IsFinitelySemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `CommRing.toRing` `Submodule.module` `LinearMap.restrict`	—	`RingHomSurjective.ids` `Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule` `RingHomInvPair.ids` `LinearEquiv.isSemisimple_iff` `RingHomCompTriple.ids` `Module.Finite.map`

Module.End.IsSemisimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_of_commute` 📖	mathematical	`Commute` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.instAdd` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`of_mem_adjoin_pair` `AddMemClass.add_mem` `smulCommClass_self` `IsScalarTower.left` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Algebra.subset_adjoin`
`aeval` 📖	mathematical	—	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Polynomial.semiring` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Polynomial.aeval`	—	`smulCommClass_self` `IsScalarTower.left` `IsScalarTower.right` `PowerBasis.finite` `minpoly.monic` `Algebra.IsIntegral.isIntegral` `Module.End.isIntegral` `Ideal.isRadical_iff_quotient_reduced` `IsSemisimpleModule.annihilator_isRadical` `Polynomial.span_minpoly_eq_annihilator` `Module.End.isSemisimple_of_squarefree_aeval_eq_zero` `Ideal.instIsTwoSided_1` `IsRadical.squarefree` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `instIsDomain` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsIntegral.of_finite` `minpoly.isRadical` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `minpoly.ker_aeval_eq_span_minpoly` `Ideal.span.eq_1` `Ideal.Quotient.liftₐ_comp` `Polynomial.aeval_algHom` `AlgHom.comp_apply` `Polynomial.aeval_algHom_apply` `minpoly.aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`isFinitelySemisimple` 📖	mathematical	—	`Module.End.IsFinitelySemisimple`	—	`Module.End.isFinitelySemisimple_iff'` `restrict`
`minpoly_squarefree` 📖	mathematical	—	`Squarefree` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `minpoly` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Module.End.instRing` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Semifield.toCommSemiring` `Algebra.id` `IsScalarTower.left`	—	`IsRadical.squarefree` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `instIsDomain` `smulCommClass_self` `IsScalarTower.left` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsIntegral.isIntegral` `Module.End.isIntegral` `isRadical_iff_span_singleton` `Polynomial.span_minpoly_eq_annihilator` `IsSemisimpleModule.annihilator_isRadical`
`mul_of_commute` 📖	mathematical	`Commute` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	—	`of_mem_adjoin_pair` `MulMemClass.mul_mem` `smulCommClass_self` `IsScalarTower.left` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `Algebra.subset_adjoin`
`of_mem_adjoin_pair` 📖	mathematical	`Commute` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Subalgebra` `Semifield.toCommSemiring` `Module.End.instSemiring` `Module.End.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.instInsert` `Set.instSingletonSet`	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`smulCommClass_self` `IsScalarTower.left` `IsScalarTower.right` `PowerBasis.finite` `minpoly.monic` `Algebra.IsIntegral.isIntegral` `Module.End.isIntegral` `Polynomial.Monic.map` `Module.Finite.trans` `AdjoinRoot.instIsScalarTower` `IsArtinianRing.of_finite` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `FiniteDimensional.finiteDimensional_self` `Ideal.isRadical_iff_quotient_reduced` `IsSemisimpleModule.annihilator_isRadical` `Polynomial.span_minpoly_eq_annihilator` `Squarefree.isRadical` `IsArtinianRing.instDecompositionMonoidPolynomial` `Polynomial.Separable.squarefree` `Polynomial.Separable.map` `PerfectField.separable_iff_squarefree` `minpoly_squarefree` `Ideal.instIsTwoSided_1` `Ideal.span.eq_1` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `minpoly.ker_aeval_eq_span_minpoly` `Polynomial.induction_on` `Polynomial.aeval_C` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Commute.add_left` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Polynomial.aeval_X` `pow_succ` `mul_assoc` `Commute.mul_left` `Ideal.span_singleton_le_iff_mem` `Polynomial.eval₂_map` `AlgHom.comp_algebraMap_of_tower` `Ideal.Quotient.isScalarTower` `Polynomial.isScalarTower` `LinearMap.instIsScalarTower` `minpoly.aeval` `Algebra.adjoin_le` `Polynomial.eval₂_C` `Polynomial.eval₂_X` `AlgHom.mem_range` `Module.End.isSemisimple_of_squarefree_aeval_eq_zero` `IsRadical.squarefree` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `instIsDomain` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsIntegral.of_finite` `minpoly.isRadical` `Polynomial.aeval_algHom` `AlgHom.comp_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`of_mem_adjoin_singleton` 📖	mathematical	`Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Subalgebra` `Semifield.toCommSemiring` `Module.End.instSemiring` `Module.End.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`	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`smulCommClass_self` `IsScalarTower.left` `Algebra.adjoin_singleton_eq_range_aeval` `aeval`
`pow` 📖	mathematical	—	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Monoid.toPow` `Module.End.instMonoid`	—	`of_mem_adjoin_singleton` `pow_mem` `smulCommClass_self` `IsScalarTower.left` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `Algebra.self_mem_adjoin_singleton`
`restrict` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule`	`Module.End.IsSemisimple` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `CommRing.toRing` `Submodule.module` `LinearMap.restrict`	—	`eq_1` `smulCommClass_self` `IsScalarTower.left` `Module.End.apply_isScalarTower` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `RingHomSurjective.ids` `RingHomInvPair.ids` `isSemisimpleModule_iff` `OrderIso.complementedLattice_iff` `IsModularLattice.complementedLattice_Iic` `Submodule.instIsModularLattice` `IsSemisimpleModule.toComplementedLattice`
`sub_of_commute` 📖	mathematical	`Commute` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Module.End.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.instSub` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`of_mem_adjoin_pair` `sub_mem` `smulCommClass_self` `IsScalarTower.left` `SubringClass.addSubgroupClass` `Subalgebra.instSubringClass` `Algebra.subset_adjoin`

---

← Back to Index