coeff_single_one_mul — Mathlib

English

For f ∈ SkewMonoidAlgebra k G, r ∈ k and x ∈ G, we have (single 1 r * f).coeff x = r * f.coeff x.

Русский

Для f ∈ SkewMonoidAlgebra k G, r ∈ k и x ∈ G имеем (single 1 r * f).coeff x = r * f.coeff x.

LaTeX

$$$ (\mathrm{single}\; 1\; r) * f .\mathrm{coeff}(x) = r \cdot f .\mathrm{coeff}(x) $$$

Lean4

theorem coeff_single_one_mul (f : SkewMonoidAlgebra k G) (r : k) (x : G) :
    (single (1 : G) r * f).coeff x = r * f.coeff x := by simp [coeff_single_mul_aux, one_smul]

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