floor_sub_ofNat — Mathlib

English

If a ≥ 0 and n ≥ 2, then ⌊a − ofNat(n)⌋₊ = ⌊a⌋₊ − ofNat(n).

Русский

Пусть a ≥ 0 и n ≥ 2. Тогда ⌊a − ofNat(n)⌋₊ = ⌊a⌋₊ − ofNat(n).

LaTeX

$$$$ \\lfloor a - \\operatorname{ofNat}(n) \\rfloor_+ = \\lfloor a \\rfloor_+ - \\operatorname{ofNat}(n) $$$$

Lean4

@[simp]
theorem floor_sub_ofNat [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [n.AtLeastTwo] :
    ⌊a - ofNat(n)⌋₊ = ⌊a⌋₊ - ofNat(n) :=
  floor_sub_natCast a n

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