Mathlib Map

Theorems · Definition · number theory

PosNum.below

{motive : PosNum → Sort u} → PosNum → Sort (max 1 u)
Defined in
Mathlib.Data.Num.Basic
Cited by
10 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 · cited by 16PosNum.brecOnPosNum.brecOn.go · cited by 10brecOn.goPosNum.brecOn.eq · cited by 9brecOn.eqPosNum.cmp.eq_def · cited by 1cmp.eq_defComputability.encodePosNum.eq_def · cited by 1encodePosNum.eq_defPosNum.divMod.eq_def · cited by 1divMod.eq_defPosNum.succ.eq_def · cited by 0succ.eq_defTuring.PartrecToTM2.trPosNum.eq_def · cited by 0trPosNum.eq_defPosNum.natSize.eq_def · cited by 0natSize.eq_defPosNum.size.eq_def · cited by 0size.eq_defPosNum.testBit.eq_def · cited by 0testBit.eq_defPosNum.sub'.eq_def · cited by 0sub'.eq_defPosNum · cited by 171PosNumPosNum.belowCITED 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 by12

Results whose statement or proof uses this declaration.