Theorems · Theorem · group theory
WithZero.unzeroD_eq_iff
∀ {α : Type u} {d y : α} {x : WithZero α}, WithZero.unzeroD d x = y ↔ x = ↑y ∨ x = 0 ∧ y = d- Defined in
- Mathlib.Algebra.Group.WithOne.Defs
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
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.
- WithZerostatement and proof · cited by 586
- WithZero.coestatement · 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.zero_ne_coeproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- WithZero.unzeroD_eq_unzeroproof · cited by 2
- WithZero.unzeroD_eq_self_iffproof · cited by 1
- WithZero.unzeroD_eq_unzeroD_iffproof · cited by 0