Documentation Verification Report

Semisimple

📁 Source: Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean

Statistics

Metric	Count
Definitions	0
Theorems `coe_genWeightSpace_zero_eq_span_range_u`, `instHasTrivialRadical`, `instIsIrreducible`, `isNilpotent_e`, `isNilpotent_f`, `trace_h_eq_zero`, `trace_toEnd_eq_zero`	7
Total	7

RootPairing.GeckConstruction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_genWeightSpace_zero_eq_span_range_u` 📖	mathematical	—	`LieSubmodule.toSubmodule` `Matrix` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `instFintypeSum` `Finset.Subtype.fintype` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Matrix.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `Algebra.id` `LieSubalgebra.instSetLike` `lieAlgebra` `Finite.of_fintype` `instIsDomain` `Field.toSemifield` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `cartanSubalgebra'` `Pi.addCommGroup` `LieRing.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Pi.Function.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `Matrix.instLieRingModuleForall` `LieModule.genWeightSpace` `LieSubalgebra.lieModule` `Matrix.instLieModuleForall` `LieModule.trivialIsNilpotent` `lieRingSelfModule` `instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Pi.addCommMonoid` `Set.range` `u`	—	`le_antisymm` `Finite.of_fintype` `instIsDomain` `LieSubalgebra.lieModule` `Matrix.instLieModuleForall` `LieModule.trivialIsNilpotent` `instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'` `Pi.mem_span_range_single_inl_iff` `Subtype.finite` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `smulCommClass_self` `IsScalarTower.left` `zero_smul` `sub_zero` `Pi.isScalarTower` `IsScalarTower.right` `LieModule.toEnd_matrix` `RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero` `RootPairing.pairingIn_eq_zero_iff` `instFaithfulSMulIntOfCharZero` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `CharZero.NeZero.two` `h_mem_lieAlgebra` `h_mem_cartanSubalgebra'` `h_eq_diagonal` `Matrix.diagonal_pow` `Matrix.mulVec_eq_sum` `Finset.sum_congr` `Matrix.diagonal_transpose` `IsCentralScalar.op_smul_eq_smul` `Pi.isCentralScalar` `CommSemigroup.isCentralScalar` `Finset.sum_apply` `mul_ite` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `IsDomain.to_noZeroDivisors` `isReduced_of_noZeroDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Submodule.span_le` `pow_one` `Matrix.mulVec_single` `one_smul` `apply_sum_inl_eq_zero_of_mem_span_h`
`instHasTrivialRadical` 📖	mathematical	—	`LieAlgebra.HasTrivialRadical` `Matrix` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `instFintypeSum` `Finset.Subtype.fintype` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Matrix.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `Algebra.id` `LieSubalgebra.instSetLike` `lieAlgebra` `Finite.of_fintype` `instIsDomain` `Field.toSemifield` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra`	—	`Nat.instAtLeastTwoHAddOfNat` `isEmpty_or_nonempty` `Finite.of_fintype` `instIsDomain` `LieAlgebra.instHasTrivialRadicalOfSubsingleton` `instSubsingletonSubtype_mathlib` `Matrix.subsingleton_of_empty_right` `instIsEmptySum` `instIsEmptySubtype` `LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Module.Finite.matrix` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Finite.instSum` `Subtype.finite` `LieSubalgebra.lieModule` `Matrix.instLieModuleForall` `FiniteDimensional.finiteDimensional_pi'` `instIsIrreducible` `LieModule.instIsFaithfulSubtypeMemLieSubalgebra` `LieModule.instIsFaithfulMatrixForall` `LieModule.instIsTriangularizableSubtypeMemLieSubalgebra` `LieModule.instIsTriangularizableOfIsAlgClosed` `trace_toEnd_eq_zero`
`instIsIrreducible` 📖	mathematical	—	`LieModule.IsIrreducible` `Matrix` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `instFintypeSum` `Finset.Subtype.fintype` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Matrix.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `Algebra.id` `LieSubalgebra.instSetLike` `lieAlgebra` `Finite.of_fintype` `instIsDomain` `Field.toSemifield` `LieSubalgebra.lieRing` `Pi.addCommGroup` `LieRing.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Pi.Function.module` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `Matrix.instLieRingModuleForall`	—	`Nat.instAtLeastTwoHAddOfNat` `Finite.of_fintype` `instIsDomain` `Function.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LieSubmodule.lie_mem` `Mathlib.Tactic.Contrapose.contrapose₄` `LieSubalgebra.lieModule` `Matrix.instLieModuleForall` `LieModule.trivialIsNilpotent` `instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'` `coe_genWeightSpace_zero_eq_span_range_u` `LieSubmodule.eq_bot_iff` `Submodule.mem_span_range_iff_exists_fun` `Fact.out` `Mathlib.Tactic.Contrapose.contrapose₂` `Matrix.exists_mulVec_eq_zero_iff` `e_mem_lieAlgebra` `e_lie_u` `Submodule.smul_mem_iff` `Pi.isScalarTower` `IsScalarTower.right` `Finset.sum_congr` `mul_comm` `zsmul_eq_mul` `AddCommGroup.intIsScalarTower` `SMulCommClass.smul_comm` `AddGroup.int_smulCommClass'` `lie_smul` `lie_sum` `Pi.single_eq_same` `NeZero.charZero_one` `apply_inr_eq_zero_of_mem_span_range_u` `Matrix.map_map` `Matrix.mulVec_eq_sum` `IsCentralScalar.op_smul_eq_smul` `Pi.isCentralScalar` `CommSemigroup.isCentralScalar` `Finset.sum_apply` `RootPairing.Base.cartanMatrix_map_abs` `eq_intCast` `RingHom.instRingHomClass` `zero_smul` `Finset.sum_const_zero`
`isNilpotent_e` 📖	mathematical	—	`IsNilpotent` `Matrix` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFintypeSum` `Finset.Subtype.fintype` `e` `Finite.of_fintype`	—	`Module.IsReflexive.of_isPerfPair` `RootPairing.isPerfPair_toLinearMap` `IsAddTorsionFree.of_isTorsionFree` `Module.IsReflexive.to_isTorsionFree` `IsDomain.toIsCancelMulZero` `Finite.of_fintype` `Matrix.isNilpotent_iff_forall_col` `sq` `Fintype.sum_sum_type` `Finset.sum_congr` `MulZeroClass.mul_zero` `Finset.sum_const_zero` `mul_ite` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `Finset.sum_ite_eq'` `RootPairing.ne_neg` `CharZero.NeZero.two` `add_zero` `RootPairing.nsmul_notMem_range_root` `Nat.instAtLeastTwoHAddOfNat` `two_smul` `Finset.sum_ite_of_false` `Pi.single_apply` `RingHomInvPair.ids` `RootPairing.root_reflectionPerm` `RootPairing.reflection_apply_self` `add_neg_cancel` `RootPairing.ne_zero` `Pi.single_eq_of_ne` `pow_succ` `Matrix.mulVec_single_one` `Matrix.mulVec_mulVec` `Matrix.mulVec_single` `one_smul` `smul_zero` `RootPairing.IsReduced.linearIndependent` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.eq_cons_cons` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Contrapose.contrapose₄` `RootPairing.root_eq_neg_iff` `RootPairing.indexNeg_neg` `neg_neg` `RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff`
`isNilpotent_f` 📖	mathematical	—	`IsNilpotent` `Matrix` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instFintypeSum` `Finset.Subtype.fintype` `f` `Finite.of_fintype`	—	`Finite.of_fintype` `isNilpotent_e` `pow_zero` `mul_one` `one_mul` `pow_succ` `mul_assoc` `ω_mul_f` `MulZeroClass.zero_mul` `ω_mul_ω` `MulZeroClass.mul_zero`
`trace_h_eq_zero` 📖	mathematical	—	`Matrix.trace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `instFintypeSum` `Finset.Subtype.fintype` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `h` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`neg_involutive` `Equiv.sum_comp` `eq_zero_of_neg_eq` `Int.instIsOrderedAddMonoid` `Finset.sum_congr` `RootPairing.pairingIn_reflectionPerm_self_left` `instFaithfulSMulIntOfCharZero` `Finset.sum_neg_distrib` `h_eq_diagonal` `Matrix.trace_diagonal` `Fintype.sum_sum_type` `Finset.sum_const_zero` `zero_add` `Nat.cast_zero` `Int.cast_zero`
`trace_toEnd_eq_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `RootPairing.Base.support` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `LinearMap.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.trace` `LieHom` `Matrix` `LieSubalgebra` `Matrix.instRing` `instFintypeSum` `Finset.Subtype.fintype` `Matrix.instAlgebra` `LieSubalgebra.instSetLike` `lieAlgebra` `Finite.of_fintype` `Module.End` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `Module.End.instRing` `Module.End.instAlgebra` `CommRing.toCommMonoid` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `LieSubalgebra.lieRingModule` `Matrix.instLieRingModuleForall` `LieSubalgebra.lieModule` `Matrix.instLieModuleForall` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Finite.of_fintype` `smulCommClass_self` `IsScalarTower.left` `LieSubalgebra.lieModule` `Matrix.instLieModuleForall` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `LieAlgebra.trace_toEnd_eq_zero` `Pi.isScalarTower` `IsScalarTower.right` `LieModule.toEnd_matrix` `Matrix.trace_toLin'_eq` `trace_h_eq_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Matrix.isNilpotent_trace_of_isNilpotent` `isNilpotent_e` `isNilpotent_f`

---

← Back to Index