coe_zsmulRec — Mathlib

English

For any integer z, the coercion of zsmulRec (· • ·) z f equals z • f as a function: coe(zsmulRec(·•·) z f) = z • coe(f).

Русский

Для любого целого z тождество: коe(zsmulRec(·•·) z f) = z • coe(f).

LaTeX

$$$\forall z, \ \text{coe}(\text{zsmulRec}(\cdot, z, f)) = z \cdot (\text{coe}(f))$$$

Lean4

@[simp]
theorem coe_zsmulRec : ∀ z, ⇑(zsmulRec (· • ·) z f) = z • ⇑f
  | Int.ofNat n => by rw [zsmulRec, Int.ofNat_eq_coe, coe_nsmul, natCast_zsmul]
  | Int.negSucc n => by rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]

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