Documentation Verification Report

Exp

📁 Source: Mathlib/RingTheory/Nilpotent/Exp.lean

Statistics

Metric	Count
Definitions `exp`	1
Theorems `exp_add_of_commute`, `exp_eq_sum`, `exp_mul_exp_neg_self`, `exp_neg_mul_exp_self`, `exp_smul`, `exp_smul_eq_sum`, `exp_zero`, `isNilpotent_exp_sub_one`, `isUnit_exp`, `map_exp`, `commute_exp_left_of_commute`, `exp_mul_of_derivation`	12
Total	13

IsNilpotent

Definitions

Name	Category	Theorems
`exp` 📖	CompOp	14 math math: `Module.End.exp_mul_of_derivation`, `isUnit_exp`, `map_exp`, `isNilpotent_exp_sub_one`, `exp_mul_exp_neg_self`, `exp_add_of_commute`, `exp_smul_eq_sum`, `exp_smul`, `LieDerivation.exp_map_apply`, `LieDerivation.exp_apply`, `Module.End.commute_exp_left_of_commute`, `exp_zero`, `exp_neg_mul_exp_self`, `exp_eq_sum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_add_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`exp` `Distrib.toAdd`	—	`pow_eq_zero_of_le` `exp_eq_sum` `Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero` `Finset.sum_congr` `Commute.add_pow` `Finset.smul_sum` `Nat.choose_eq_factorial_div_factorial` `Nat.cast_div` `Nat.factorial_mul_factorial_dvd_factorial` `ne_of_gt` `Nat.cast_pos'` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.factorial_pos` `Nat.cast_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Nat.cast_commute` `mul_smul_comm` `SMulCommClass.rat` `nsmul_eq_mul` `SemigroupAction.mul_smul` `smul_assoc` `AddCommMonoid.nat_isScalarTower` `SMulCommClass.smul_comm` `Nat.cast_smul_eq_nsmul` `Finset.sum_sigma'` `Finset.sum_bij` `Nat.instNoMaxOrder` `Finset.sum_eq_zero` `le_or_gt` `MulZeroClass.zero_mul` `smul_zero` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `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.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.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_add` `lt_of_not_ge` `Finset.mem_filter` `Nat.cast_one` `MulZeroClass.mul_zero` `Finset.sum_filter_add_sum_filter_not` `Finset.filter.congr_simp` `Finset.ext` `Finset.sum_mul_sum` `smul_mul_assoc` `IsScalarTower.rat` `smul_smul` `Finset.sum_bijective` `add_zero`
`exp_eq_sum` 📖	mathematical	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`exp` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Rat.monoid` `Module.toDistribMulAction` `Rat.semiring` `Nat.factorial`	—	`Finset.sum_range_add_sum_Ico` `csInf_le'` `Finset.sum_eq_zero` `pow_eq_zero_of_le` `Finset.mem_Ico` `pow_nilpotencyClass` `smul_zero` `add_zero`
`exp_mul_exp_neg_self` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `exp` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`exp_add_of_commute` `Commute.neg_right` `neg` `add_neg_cancel` `exp_zero`
`exp_neg_mul_exp_self` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `exp` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`exp_add_of_commute` `Commute.neg_left` `neg` `neg_add_cancel` `exp_zero`
`exp_smul` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`exp` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction`	—	`map_exp` `RingHom.instRingHomClass`
`exp_smul_eq_sum` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Monoid.toNatPow` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`exp` `Finset.sum` `Finset.range` `Rat.monoid` `Rat.semiring` `Nat.factorial`	—	`le_or_gt` `exp_eq_sum` `pow_eq_zero_of_le` `pow_nilpotencyClass` `Finset.sum_smul` `Finset.sum_congr` `smul_assoc` `IsScalarTower.rat` `exp.eq_1` `Finset.sum_range_add_sum_Ico` `Finset.sum_eq_zero` `pow_sub_mul_pow` `Finset.mem_Ico` `SemigroupAction.mul_smul` `smul_zero` `add_zero`
`exp_zero` 📖	mathematical	—	`exp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`exp_eq_sum` `pow_one` `Finset.sum_singleton` `Nat.cast_one` `inv_one` `pow_zero` `one_smul`
`isNilpotent_exp_sub_one` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `exp` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `exp.eq_1` `pos_nilpotencyClass_iff` `Finset.sum_range_succ'` `Finset.sum_congr` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_natSucc` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `inv_one` `pow_zero` `one_smul` `add_sub_cancel_right` `Commute.isNilpotent_sum` `smul` `SMulCommClass.rat` `IsScalarTower.rat` `pow_of_pos` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Rat.instCharZero`
`isUnit_exp` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsUnit` `exp`	—	`isUnit_iff_exists` `exp_mul_exp_neg_self` `exp_neg_mul_exp_self`
`map_exp` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`DFunLike.coe` `exp`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `exp_eq_sum` `map_sum` `RingHomClass.toAddMonoidHomClass` `Finset.sum_congr` `map_rat_smul` `map_pow`

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_exp_left_of_commute` 📖	mathematical	`IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `instMonoid` `LinearMap.comp` `RingHomCompTriple.ids`	`IsNilpotent.exp` `LinearMap` `instRing` `LinearMap.module` `Rat.semiring` `SMulCommClass.rat'` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction`	—	`RingHomCompTriple.ids` `LinearMap.ext` `SMulCommClass.rat'` `pow_eq_zero_of_le` `LinearMap.congr_fun` `RingHomCompTriple.right_ids` `commute_pow_left_of_commute` `LinearMap.comp.congr_simp` `IsNilpotent.exp_eq_sum` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_rat_smul`
`exp_mul_of_derivation` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `LinearMap.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `IsNilpotent` `LinearMap.instZero` `Monoid.toNatPow` `instMonoid`	`IsNilpotent.exp` `instRing` `NonUnitalNonAssocRing.toAddCommGroup` `LinearMap.module` `Rat.semiring` `SMulCommClass.rat'` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction`	—	`IsNilpotent.map` `smulCommClass_self` `IsScalarTower.left` `TensorProduct.smulCommClass_left` `TensorProduct.isScalarTower` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `TensorProduct.AlgebraTensorModule.curry_injective` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `SMulCommClass.rat'` `RingHomCompTriple.ids` `commute_exp_left_of_commute` `Commute.isNilpotent_add` `LinearMap.comp.congr_simp` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `LinearMap.congr_fun` `IsNilpotent.map_exp` `IsNilpotent.exp_add_of_commute`

---

← Back to Index