Theorems · Definition · group theory
WithZero.recZeroCoe
{α : Type u} → {motive : WithZero α → Sort u_1} → motive 0 → ((a : α) → motive ↑a) → (n : WithZero α) → motive nRecursor for WithZero using the preferred forms 0 and ↑a.
- Defined in
- Mathlib.Algebra.Group.WithOne.Defs
- Cited by
- 29 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.coestatement and proof · cited by 186
Cited by34
Results whose statement or proof uses this declaration.
- WithZero.logproof · cited by 40
- WithZero.unzeroDproof · cited by 14
- MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀proof · cited by 12
- WithZero.lift'proof · cited by 10
- WithZero.withZeroUnitsEquivproof · cited by 9
- WithZero.liftproof · cited by 6
- LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrderedproof · cited by 4
- WithZeroMulInt.toNNReal_strictMonoproof · cited by 4
- MonoidWithZeroHom.ValueGroup₀.embedding_applystatement · cited by 3
- WithZero.unzeroD_eq_iffproof · cited by 3
- WithZero.withZeroUnitsEquiv_applystatement · cited by 2
- AlgebraicGeometry.Scheme.ord_zeroproof · cited by 2