Theorems · Theorem · number theory

PosNum.divMod.eq_def

∀ (d x : PosNum),
  d.divMod x =
    match x with
    | n.bit0 =>
      match d.divMod n with
      | (q, r₁) => d.divModAux q r₁.bit0
    | n.bit1 =>
      match d.divMod n with
      | (q, r₁) => d.divModAux q r₁.bit1
    | PosNum.one => d.divModAux 0 1

Defined in

Mathlib.Data.Num.ZNum

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms