cast_to_znum — Mathlib

English

Every positive numeral n, when cast to ZNum, equals ZNum.pos n.

Русский

Каждое положительное число n, приведённое к ZNum, равно ZNum.pos n.

LaTeX

$$$$\forall n:\mathrm{PosNum},\ (n : \mathrm{ZNum}) = \mathrm{ZNum.pos}(n).$$$$

Lean4

theorem cast_to_znum : ∀ n : PosNum, (n : ZNum) = ZNum.pos n
  | 1 => rfl
  | bit0 p => by
    have := congr_arg ZNum.bit0 (cast_to_znum p)
    rwa [← ZNum.bit0_of_bit0] at this
  | bit1 p => by
    have := congr_arg ZNum.bit1 (cast_to_znum p)
    rwa [← ZNum.bit1_of_bit1] at this

Похожие утверждения