Theorems · Theorem · number theory
Nat.binaryRec_zero
∀ {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)),
Nat.binaryRec zero bit 0 = zero- Defined in
- Mathlib.Data.Nat.BinaryRec
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Quot.sound
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.
- Nat.bitstatement and proof · cited by 92
- Nat.binaryRecstatement · cited by 24
Cited by4
Results whose statement or proof uses this declaration.
- nsmulRec_eq_nsmulBinRecproof · cited by 1
- npowRec_eq_npowBinRecproof · cited by 1
- Nat.binaryRec'_zeroproof · cited by 1
- Nat.evenOddRec_zeroproof · cited by 0