map_smul' — Mathlib

English

If f preserves multiplication, then (r • A).map f = f(r) • (A.map f).

Русский

Если f сохраняет умножение, то (r • A).map f = f(r) • (A.map f).

LaTeX

$$$ (r \\cdot A).map\\ f = (f r) \\cdot (A.map\\ f) $$$

Lean4

/-- The scalar action via `Mul.toSMul` is transformed by the same map as the elements
of the matrix, when `f` preserves multiplication. -/
theorem map_smul' [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ a₁ a₂, f (a₁ * a₂) = f a₁ * f a₂) :
    (r • A).map f = f r • A.map f :=
  ext fun _ _ => hf _ _

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