addRothNumber_eq_rothNumberNat — Mathlib

English

If 2k ≤ n, then addRothNumber(Iio(k) in Fin n.succ) equals rothNumberNat(k).

Русский

Если 2k ≤ n, то addRothNumber(Iio(k) в Fin n.succ) равно rothNumberNat(k).

LaTeX

$$$\\operatorname{addRothNumber}(\\mathrm{Iio}(k)) = \\operatorname{rothNumberNat}(k), \\text{ при } 2k \\le n.$$$

Lean4

theorem addRothNumber_eq_rothNumberNat (hkn : 2 * k ≤ n) :
    addRothNumber (Iio k : Finset (Fin n.succ)) = rothNumberNat k :=
  IsAddFreimanIso.addRothNumber_congr <| mod_cast isAddFreimanIso_Iio two_ne_zero hkn

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