Theorems · Definition · group theory
WithZero.unzero
{α : Type u} → {x : WithZero α} → x ≠ 0 → αDeconstruct an x : WithZero α to the underlying value in α, given a proof that x ≠ 0.
- Defined in
- Mathlib.Algebra.Group.WithOne.Defs
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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.coeproof · cited by 186
Cited by41
Results whose statement or proof uses this declaration.
- WithZeroMulInt.toNNRealproof · cited by 28
- WithZero.coe_unzerostatement and proof · cited by 17
- MulEquiv.withZeroproof · cited by 6
- LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrderedproof · cited by 4
- WithZeroMulInt.toNNReal_strictMonoproof · cited by 4
- WithZero.toAdd_unzero_eq_logstatement · cited by 4
- WithZero.unitsWithZeroEquivproof · cited by 4
- WithZero.unzero.congr_simpstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.ord_eq_unzero_ordHomstatement and proof · cited by 3
- NumberField.HeightOneSpectrum.embedding_mul_absNormproof · cited by 3
- WithZeroMulInt.toNNReal_neg_applystatement and proof · cited by 2
- WithZero.exists_ne_zero_and_ltproof · cited by 2