Documentation Verification Report

Sl2

📁 Source: Mathlib/Algebra/Lie/Sl2.lean

Statistics

Metric	Count
Definitions `IsSl2Triple`, `HasPrimitiveVectorWith`, `toLieSubalgebra`	3
Theorems `exists_nat`, `lie_e`, `lie_e_pow_succ_toEnd_f`, `lie_f_pow_toEnd_f`, `lie_h`, `lie_h_pow_toEnd_f`, `mk'`, `ne_zero`, `pow_toEnd_f_eq_zero_of_eq_nat`, `pow_toEnd_f_ne_zero_of_eq_nat`, `e_ne_zero`, `f_ne_zero`, `h_ne_zero`, `lie_e_f`, `lie_h_e_nsmul`, `lie_h_e_smul`, `lie_h_f_nsmul`, `lie_lie_smul_f`, `mem_toLieSubalgebra_iff`, `symm_iff`	20
Total	23

IsSl2Triple

Definitions

Name	Category	Theorems
`HasPrimitiveVectorWith` 📖	CompData	1 math math: `HasPrimitiveVectorWith.mk'`
`toLieSubalgebra` 📖	CompOp	1 math math: `mem_toLieSubalgebra_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`e_ne_zero` 📖	—	`IsSl2Triple`	—	—	`h_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `zero_lie` `lie_e_f`
`f_ne_zero` 📖	—	`IsSl2Triple`	—	—	`h_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `lie_zero` `lie_e_f`
`h_ne_zero` 📖	—	`IsSl2Triple`	—	—	—
`lie_e_f` 📖	mathematical	`IsSl2Triple`	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	—
`lie_h_e_nsmul` 📖	mathematical	`IsSl2Triple`	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`lie_h_e_smul` 📖	mathematical	`IsSl2Triple`	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `LieAlgebra.toModule` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `lie_h_e_nsmul` `two_smul`
`lie_h_f_nsmul` 📖	mathematical	`IsSl2Triple`	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`lie_lie_smul_f` 📖	mathematical	`IsSl2Triple`	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `LieAlgebra.toModule` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `lie_h_f_nsmul` `two_smul` `neg_add_rev`
`mem_toLieSubalgebra_iff` 📖	mathematical	`IsSl2Triple`	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `toLieSubalgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `LieAlgebra.toModule` `Bracket.bracket` `LieRingModule.toBracket` `lieRingSelfModule`	—	`lie_e_f`
`symm_iff` 📖	mathematical	—	`IsSl2Triple` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	`symm` `neg_neg`

IsSl2Triple.HasPrimitiveVectorWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nat` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`smulCommClass_self` `IsScalarTower.left` `Nat.instAtLeastTwoHAddOfNat` `Set.infinite_range_iff` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `instInfiniteNat` `LinearIndependent.finite` `commRing_strongRankCondition` `instNontrivialOfCharZero` `Module.IsNoetherian.finite` `Module.End.eigenvectors_linearIndependent` `lie_h_pow_toEnd_f` `Nat.exists_not_and_succ_of_not_zero_of_exists` `ne_zero` `lie_e_pow_succ_toEnd_f` `sub_eq_zero` `mul_eq_zero` `IsDomain.to_noZeroDivisors` `smul_eq_zero_iff_left` `lie_zero` `Nat.cast_add_one_ne_zero`
`lie_e` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	`Bracket.bracket` `LieRingModule.toBracket` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`lie_e_pow_succ_toEnd_f` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	`Bracket.bracket` `LieRingModule.toBracket` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.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` `LieHom.instFunLike` `LieModule.toEnd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `SubNegMonoid.toSub` `AddGroupWithOne.toAddGroup`	—	`smulCommClass_self` `IsScalarTower.left` `zero_add` `pow_one` `leibniz_lie` `instIsLieTower` `IsSl2Triple.lie_e_f` `lie_h` `lie_e` `lie_zero` `add_zero` `Nat.cast_zero` `sub_zero` `one_mul` `pow_zero` `pow_succ'` `Module.End.mul_apply` `LieModule.toEnd_apply_apply` `Nat.instAtLeastTwoHAddOfNat` `lie_h_pow_toEnd_f` `lie_smul` `lie_f_pow_toEnd_f` `add_smul` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `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_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add`
`lie_f_pow_toEnd_f` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	`Bracket.bracket` `LieRingModule.toBracket` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.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` `LieHom.instFunLike` `LieModule.toEnd`	—	`smulCommClass_self` `IsScalarTower.left` `pow_succ'`
`lie_h` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	`Bracket.bracket` `LieRingModule.toBracket` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	—
`lie_h_pow_toEnd_f` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	`Bracket.bracket` `LieRingModule.toBracket` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.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` `LieHom.instFunLike` `LieModule.toEnd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `SubNegMonoid.toSub` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`smulCommClass_self` `IsScalarTower.left` `Nat.instAtLeastTwoHAddOfNat` `pow_zero` `Nat.cast_zero` `MulZeroClass.mul_zero` `sub_zero` `lie_h` `pow_succ'` `Module.End.mul_apply` `LieModule.toEnd_apply_apply` `Nat.cast_add` `Nat.cast_one` `leibniz_lie` `instIsLieTower` `IsSl2Triple.lie_lie_smul_f` `neg_smul` `lie_smul` `smul_lie` `add_smul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt`
`mk'` 📖	mathematical	`IsSl2Triple` `Bracket.bracket` `LieRingModule.toBracket` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`IsSl2Triple.HasPrimitiveVectorWith`	—	`nsmul_lie` `IsSl2Triple.lie_h_e_nsmul` `lie_lie` `lie_smul` `smul_smul` `mul_comm` `sub_self` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`ne_zero` 📖	—	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith`	—	—	—
`pow_toEnd_f_eq_zero_of_eq_nat` 📖	mathematical	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smulCommClass_self` `IsScalarTower.left` `Nat.instAtLeastTwoHAddOfNat` `lie_h_pow_toEnd_f` `Nat.cast_add` `Nat.cast_one` `lie_e_pow_succ_toEnd_f` `sub_self` `MulZeroClass.mul_zero` `zero_smul` `exists_nat` `LT.lt.ne` `Int.cast_injective` `Int.cast_natCast` `Int.cast_add` `Int.cast_mul` `Int.cast_ofNat` `Int.cast_one`
`pow_toEnd_f_ne_zero_of_eq_nat` 📖	—	`IsSl2Triple` `IsSl2Triple.HasPrimitiveVectorWith` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—	`smulCommClass_self` `IsScalarTower.left` `ne_zero` `pow_zero` `Int.cast_smul_eq_zsmul` `Int.cast_mul` `Int.cast_add` `Int.cast_natCast` `Int.cast_one` `Int.cast_sub` `IsDomain.toIsCancelMulZero` `IsDomain.to_noZeroDivisors` `lie_e_pow_succ_toEnd_f` `lie_zero` `LE.le.not_gt` `LE.le.trans_eq` `Unique.instSubsingleton` `Nat.cast_eq_zero` `Int.instCharZero` `Nat.cast_add` `Nat.cast_one` `sub_eq_zero` `mul_eq_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Int.cast_eq_zero` `smul_eq_zero` `LE.le.trans`

(root)

Definitions

Name	Category	Theorems
`IsSl2Triple` 📖	CompData	3 math math: `RootPairing.GeckConstruction.isSl2Triple`, `IsSl2Triple.symm_iff`, `LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero`

---

← Back to Index