multipliable_pnat_iff_multipliable_succ

English

Multipliable on the positive naturals equals Multipliable on the standard naturals shifted by 1.

Русский

Умножимость на положительных натуральных равна умножимости на натуральных сдвинутых на 1.

LaTeX

$$$\\displaystyle \\text{Multipliable}(n \\mapsto f(n)) \\iff \\text{Multipliable}(n \\mapsto f(n+1))$$$

Lean4

@[to_additive]
theorem multipliable_pnat_iff_multipliable_succ {f : ℕ → M} :
    Multipliable (fun x : ℕ+ ↦ f x) ↔ Multipliable fun x ↦ f (x + 1) :=
  Equiv.pnatEquivNat.symm.multipliable_iff.symm

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