Theorems · Theorem · group theory
IsNilpotent.eq_zero
∀ {R : Type u_3} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [IsReduced R], IsNilpotent x → x = 0- Defined in
- Mathlib.Algebra.GroupWithZero.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsNilpotentstatement and proof · cited by 248
- IsReducedstatement and proof · cited by 98
- IsReduced.eq_zeroproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- isNilpotent_iff_eq_zeroproof · cited by 9
- isReduced_of_injectiveproof · cited by 7
- Algebra.FormallyUnramified.isReduced_of_fieldproof · cited by 6
- LieModule.trace_toEnd_genWeightSpaceproof · cited by 3
- IsNilpotent.charpoly_eq_X_pow_finrankproof · cited by 2
- AlgebraicGeometry.isReduced_of_isReduced_stalkproof · cited by 1
- Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparableproof · cited by 1
- AlgebraicGeometry.eq_zero_of_basicOpen_eq_botproof · cited by 1
- LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebraproof · cited by 1
- Matrix.isParabolic_iff_existsproof · cited by 1
- LieModule.Weight.apply_eq_zero_of_isNilpotentproof · cited by 0
- isReduced_localizationPreservesproof · cited by 0