Theorems · Theorem · commutative algebra
DualNumber.isNilpotent_iff_eps_dvd
∀ {R : Type u_1} [inst : DivisionSemiring R] {x : DualNumber R}, IsNilpotent x ↔ DualNumber.eps ∣ x- Defined in
- Mathlib.RingTheory.DualNumber
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOppositestatement · cited by 1,135
- IsNilpotentstatement · cited by 248
- DivisionSemiringstatement and proof · cited by 216
- DualNumberstatement and proof · cited by 52
- DualNumber.epsstatement and proof · cited by 30
Cited by2
Results whose statement or proof uses this declaration.
- DualNumber.ideal_trichotomyproof · cited by 1
- DualNumber.exists_mul_left_or_mul_rightproof · cited by 0