Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions `nilradical`	1
Theorems `isNilpotent_mulLeft_iff`, `isNilpotent_mulRight_iff`, `isNilpotent_toMatrix_iff`, `isNilpotent_toLin'_iff`, `mapQ`, `restrict`, `isNilpotent_restrict_of_le`, `ker_isRadical_iff_reduced_of_surjective`, `isNilpotent_iff_zero_mem_powers`, `isRadical_iff_span_singleton`, `mem_nilradical`, `nilpotent_iff_mem_prime`, `nilradical_eq_bot_iff`, `nilradical_eq_sInf`, `nilradical_eq_zero`, `nilradical_le_prime`	16
Total	17

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_mulLeft_iff` 📖	mathematical	—	`IsNilpotent` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `instZero` `Monoid.toNatPow` `Module.End.instMonoid` `mulLeft` `Algebra.to_smulCommClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Algebra.to_smulCommClass` `pow_mulLeft`
`isNilpotent_mulRight_iff` 📖	mathematical	—	`IsNilpotent` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `instZero` `Monoid.toNatPow` `Module.End.instMonoid` `mulRight` `IsScalarTower.right` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsScalarTower.right` `pow_mulRight`
`isNilpotent_toMatrix_iff` 📖	mathematical	—	`IsNilpotent` `Matrix` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `LinearMap` `addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype` `instZero` `Module.End.instMonoid`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `toMatrix_pow` `LinearEquiv.map_eq_zero_iff`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_toLin'_iff` 📖	mathematical	—	`IsNilpotent` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instZero` `Monoid.toNatPow` `Module.End.instMonoid` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `semiring`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Function.smulCommClass` `Algebra.to_smulCommClass` `LinearMap.toMatrix'_toLin'` `LinearMap.isNilpotent_toMatrix_iff`

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_restrict_of_le` 📖	—	`Set.MapsTo` `DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `SetLike.coe` `Submodule` `Submodule.setLike` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `IsNilpotent` `LinearMap` `SetLike.instMembership` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instZero` `Monoid.toNatPow` `instMonoid` `LinearMap.restrict`	—	—	`LinearMap.ext` `DFunLike.congr_fun` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `pow_apply_mem_of_forall_mem` `pow_restrict` `LinearMap.restrict_apply`

Module.End.IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapQ` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.comap` `RingHom.id` `Semiring.toNonAssocSemiring` `IsNilpotent` `Module.End` `LinearMap.instZero` `Monoid.toNatPow` `Module.End.instMonoid`	`LinearMap` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.mapQ`	—	`Submodule.le_comap_pow_of_le_comap` `Submodule.mapQ_pow` `Submodule.mapQ.congr_simp` `Submodule.mapQ_zero`

Module.End.isNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrict` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `IsNilpotent` `LinearMap.instZero` `Monoid.toNatPow` `Module.End.instMonoid`	`SetLike.instMembership` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.restrict`	—	`LinearMap.ext` `Module.End.pow_apply_mem_of_forall_mem` `Module.End.pow_restrict` `LinearMap.restrict.congr_simp`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_isRadical_iff_reduced_of_surjective` 📖	mathematical	`DFunLike.coe`	`Ideal.IsRadical` `ker` `CommSemiring.toSemiring` `IsReduced` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Function.Surjective.forall` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`

(root)

Definitions

Name	Category	Theorems
`nilradical` 📖	CompOp	23 math math: `PrimeSpectrum.zeroLocus_nilradical`, `PrimeSpectrum.zeroLocus_eq_univ_iff`, `Ring.jacobson_eq_nilradical_of_krullDimLE_zero`, `AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical`, `PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical`, `PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical`, `pNilradical_prime`, `nilradical_le_prime`, `nilradical_eq_zero`, `Ring.krullDimLE_zero_and_isLocalRing_tfae`, `Ring.KrullDimLE.nilradical_eq_maximalIdeal`, `nilradical_le_jacobson`, `pNilradical_eq_nilradical`, `AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact`, `IsNoetherianRing.isNilpotent_nilradical`, `PrimeSpectrum.vanishingIdeal_univ`, `PrimeSpectrum.nilradical_eq_iInf`, `Ideal.FG.isNilpotent_iff_le_nilradical`, `nilradical_eq_bot_iff`, `nilradical_eq_sInf`, `IsArtinianRing.isNilpotent_nilradical`, `pNilradical_le_nilradical`, `mem_nilradical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_iff_zero_mem_powers` 📖	mathematical	—	`IsNilpotent` `Monoid.toNatPow` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers`	—	—
`isRadical_iff_span_singleton` 📖	mathematical	—	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Ideal.IsRadical` `Ideal.span` `Set` `Set.instSingletonSet`	—	`forall_swap`
`mem_nilradical` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `nilradical` `IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`nilpotent_iff_mem_prime` 📖	mathematical	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule`	—	`mem_nilradical` `nilradical_eq_sInf` `Submodule.mem_sInf`
`nilradical_eq_bot_iff` 📖	mathematical	—	`nilradical` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsReduced` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`instIsConcreteLE`
`nilradical_eq_sInf` 📖	mathematical	—	`nilradical` `InfSet.sInf` `Ideal` `CommSemiring.toSemiring` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setOf` `Ideal.IsPrime`	—	`Ideal.radical_eq_sInf` `bot_le`
`nilradical_eq_zero` 📖	mathematical	—	`nilradical` `Ideal` `CommSemiring.toSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.ext` `isNilpotent_iff_eq_zero`
`nilradical_le_prime` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `nilradical`	—	`sInf_le` `nilradical_eq_sInf`

---

← Back to Index