nfp_add_zero — Mathlib

English

For any a, nfp (a + ·) 0 = a · ω.

Русский

Для любого a, nfp (a + ·) 0 = a · ω.

LaTeX

$$$$ \operatorname{nfp}(a + \cdot) 0 = a \cdot \omega $$$$

Lean4

@[simp]
theorem nfp_add_zero (a) : nfp (a + ·) 0 = a * ω :=
  by
  simp_rw [← iSup_iterate_eq_nfp, ← iSup_mul_nat]
  congr; funext n
  induction n with
  | zero => rw [Nat.cast_zero, mul_zero, iterate_zero_apply]
  | succ n hn => rw [iterate_succ_apply', Nat.add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, hn]

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