Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `add_pow_add_eq_zero_of_pow_eq_zero`, `add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero`, `isNilpotent_add`, `isNilpotent_finsum`, `isNilpotent_mul_left_iff`, `isNilpotent_mul_right_iff`, `isNilpotent_sub`, `isNilpotent_sum`, `eq_zero_of_isNilpotent`, `eq_zero_of_isIdempotentElem`, `isUnit_add_left_of_commute`, `isUnit_add_one`, `isUnit_add_right_of_commute`, `isUnit_one_add`, `isUnit_one_sub`, `isUnit_sub_one`, `neg`, `not_isUnit`, `smul`, `of_dvd`, `not_isNilpotent`, `isReduced`, `isRadical`, `instIsReducedProd`, `isNilpotent_finsum`, `isNilpotent_neg_iff`, `isNilpotent_sum`, `isReduced_iff_pow_one_lt`, `zero_isRadical_iff`	29
Total	29

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow_add_eq_zero_of_pow_eq_zero` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Distrib.toAdd`	—	`add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero` `le_refl`
`add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Distrib.toAdd`	—	`add_pow'` `Finset.sum_eq_zero` `pow_eq_zero_of_le` `MulZeroClass.zero_mul` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `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.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `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` `Nat.cast_one` `lt_of_not_ge` `neg_eq_zero` `sub_eq_zero_of_eq` `Finset.HasAntidiagonal.mem_antidiagonal` `MulZeroClass.mul_zero` `nsmul_eq_mul`
`isNilpotent_add` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd`	—	`add_pow_add_eq_zero_of_pow_eq_zero`
`isNilpotent_finsum` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`finsum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`finsum_def` `isNilpotent_sum`
`isNilpotent_mul_left_iff` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsLeft`	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`Submonoid.pow_mem` `mul_pow` `isNilpotent_mul_left`
`isNilpotent_mul_right_iff` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsRight`	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`Submonoid.pow_mem` `mul_pow` `isNilpotent_mul_right`
`isNilpotent_sub` 📖	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`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg` `isNilpotent_add` `neg_right_iff` `isNilpotent_neg_iff`
`isNilpotent_sum` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.induction` `Finset.sum_insert` `isNilpotent_add` `sum_right`

IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_isNilpotent` 📖	—	`IsIdempotentElem` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsNilpotent` `MulZeroClass.toZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	—	`one_mul` `pow_zero` `MulZeroClass.zero_mul` `pow_succ_eq`

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_isIdempotentElem` 📖	—	`IsIdempotentElem` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsNilpotent` `MulZeroClass.toZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	—	`IsIdempotentElem.eq_zero_of_isNilpotent`
`isUnit_add_left_of_commute` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `IsUnit` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Distrib.toAdd`	—	`Units.isUnit_mul_units` `add_mul` `Distrib.rightDistribClass` `IsUnit.mul_val_inv` `Commute.units_inv_right` `isUnit_one_add` `IsUnit.isNilpotent_mul_unit_of_commute_iff` `Units.isUnit`
`isUnit_add_one` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsUnit` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`IsUnit.neg_iff` `neg_add'` `isUnit_sub_one` `neg`
`isUnit_add_right_of_commute` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `IsUnit` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Distrib.toAdd`	—	`isUnit_add_left_of_commute` `add_comm`
`isUnit_one_add` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsUnit` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`isUnit_add_one` `add_comm`
`isUnit_one_sub` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsUnit` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsUnit.neg_iff` `neg_sub` `isUnit_sub_one`
`isUnit_sub_one` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsUnit` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`mul_neg` `mul_geom_sum` `zero_sub` `neg_neg` `neg_mul` `geom_sum_mul`
`neg` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`neg_pow` `MulZeroClass.mul_zero`
`not_isUnit` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsUnit`	—	`IsUnit.not_isNilpotent`
`smul` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulActionWithZero.toSMulWithZero`	—	`smul_pow` `smul_zero`

IsRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_dvd` 📖	—	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	—	`isRadical_iff_pow_one_lt` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_dvd_mul_iff_right` `right_ne_zero_of_mul` `mul_pow` `mul_dvd_mul` `dvd_pow_self` `two_ne_zero`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isNilpotent` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow`	—	`add_neg_cancel` `NeZero.one` `IsNilpotent.isUnit_add_right_of_commute` `neg`

NoZeroSMulDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isReduced` 📖	mathematical	—	`IsReduced` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`isReduced_of_noZeroDivisors`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRadical` 📖	mathematical	`Prime`	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`dvd_of_dvd_pow`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsReducedProd` 📖	mathematical	—	`IsReduced` `Prod.instZero` `Prod.instPow`	—	`IsReduced.eq_zero`
`isNilpotent_finsum` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`finsum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Commute.isNilpotent_finsum` `Commute.all`
`isNilpotent_neg_iff` 📖	mathematical	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`IsNilpotent.neg` `neg_neg`
`isNilpotent_sum` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Commute.isNilpotent_sum` `Commute.all`
`isReduced_iff_pow_one_lt` 📖	mathematical	—	`IsReduced` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`isRadical_iff_pow_one_lt`
`zero_isRadical_iff` 📖	mathematical	—	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsReduced`	—	`forall_swap`

---

← Back to Index