dvd_coord_smul — Mathlib

English

For any i, m ∈ M, and r ∈ R, the i-th coordinate respects scalar multiplication: b.coord i (r • m) = r • b.coord i m.

Русский

Для любого i, m ∈ M и r ∈ R координата по i-му базису уважает умножение на скаляр: b.coord i (r • m) = r • b.coord i m.

LaTeX

$$$ b.coord\,i\ (r\cdot m) = r\cdot b.coord\,i\ m $$$

Lean4

theorem dvd_coord_smul (i : ι) (m : M) (r : R) : r ∣ b.coord i (r • m) :=
  ⟨b.coord i m, by simp⟩

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