Theorems · Theorem · group theory
WithZero.unzeroD_eq_unzeroD_iff
∀ {α : Type u} {d : α} {x y : WithZero α},
WithZero.unzeroD d x = WithZero.unzeroD d y ↔ x = y ∨ x = ↑d ∧ y = 0 ∨ x = 0 ∧ y = ↑d- Defined in
- Mathlib.Algebra.Group.WithOne.Defs
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- WithZerostatement and proof · cited by 586
- WithZero.coestatement and proof · cited by 186
- WithZero.recZeroCoeproof · cited by 29
- WithZero.unzeroDstatement · cited by 14
- WithZero.coe_ne_zeroproof · cited by 11
- WithZero.coe_injproof · cited by 6
- WithZero.unzeroD_eq_iffproof · cited by 3
- WithZero.zero_ne_coeproof · cited by 2
- WithZero.unzeroD_eq_self_iffproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.