cast_mul_eq_zsmul_cast — Mathlib

English

For any α with AddGroupWithOne, and integers m,n, the cast of m·n equals m acting on the cast of n: (m n)^{↑} = m · (n^{↑}).

Русский

Для любого α с AddGroupWithOne и целых m, n выполняется: (m·n)^{↑} = m · (n^{↑}).

LaTeX

$$$ (m \cdot n)^{\uparrow} = m \cdot (n^{\uparrow}) $$$

Lean4

/-- Note this holds in marginally more generality than `Int.cast_mul` -/
theorem cast_mul_eq_zsmul_cast {α : Type*} [AddGroupWithOne α] : ∀ m n : ℤ, ↑(m * n) = m • (n : α) := fun m ↦
  Int.induction_on m (by simp) (fun _ ih ↦ by simp [add_mul, add_zsmul, ih]) fun _ ih ↦ by
    simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]

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