Mathlib Map

Theorems · Definition · number theory

PosNum.casesOn

{motive : PosNum → Sort u} →
  (t : PosNum) → motive PosNum.one → ((a : PosNum) → motive a.bit1) → ((a : PosNum) → motive a.bit0) → motive t
Defined in
Mathlib.Data.Num.Basic
Cited by
17 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PosNum.brecOn.eq · cited by 9brecOn.eqNum.add_one · cited by 7Num.add_onePosNum.add_one · cited by 4PosNum.add_oneNum.castNum_eq_bitwise · cited by 4Num.castNum_eq_bitwiseZNum.add_one · cited by 3ZNum.add_oneComputability.encodePosNum_nonempty · cited by 2Computability.encodePosNu…PosNum.cmp_swap · cited by 2PosNum.cmp_swapTuring.PartrecToTM2.pred_ok · cited by 1PartrecToTM2.pred_okPosNum.minFac_to_nat · cited by 1PosNum.minFac_to_natTuring.PartrecToTM2.tr_ret_respects · cited by 1PartrecToTM2.tr_ret_respe…PosNum.one_sub' · cited by 1PosNum.one_sub'PosNum.sub'_one · cited by 0PosNum.sub'_oneNum.castNum_or · cited by 0Num.castNum_orPosNum.natSize_pos · cited by 0PosNum.natSize_posNum.castNum_shiftRight · cited by 0Num.castNum_shiftRightPosNum · cited by 171PosNumPosNum.casesOnCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PosNumstatement and proof · cited by 171

Cited by21

Results whose statement or proof uses this declaration.