Theorems · Theorem · commutative algebra
IsNilpotent.map
∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] {r : R} {F : Type u_3}
[inst_2 : FunLike F R S] [MonoidWithZeroHomClass F R S], IsNilpotent r → ∀ (f : F), IsNilpotent (f r)- Defined in
- Mathlib.RingTheory.Nilpotent.Defs
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- map_zeroproof · cited by 1,614
- map_powproof · cited by 503
- MonoidWithZerostatement and proof · cited by 456
- IsNilpotentstatement and proof · cited by 248
- MonoidWithZeroHomClassstatement and proof · cited by 37
Cited by12
Results whose statement or proof uses this declaration.
- IsNilpotent.map_iffproof · cited by 9
- isReduced_of_injectiveproof · cited by 7
- Algebra.FormallyUnramified.isReduced_of_fieldproof · cited by 6
- IsNilpotent.charpoly_eq_X_pow_finrankproof · cited by 2
- PrimeSpectrum.mem_image_comap_zeroLocus_sdiffproof · cited by 2
- MvPowerSeries.IsNilpotent_substproof · cited by 1
- Algebra.isNilpotent_trace_of_isNilpotentproof · cited by 1
- MvPowerSeries.HasSubst.mapproof · cited by 1
- AlgebraicGeometry.isReduced_of_isReduced_stalkproof · cited by 1
- AlgebraicGeometry.eq_zero_of_basicOpen_eq_botproof · cited by 1
- isReduced_ofLocalizationMaximalproof · cited by 0
- Module.End.exp_mul_of_derivationproof · cited by 0