coeff_mul_single_one — Mathlib

English

Given f ∈ SkewMonoidAlgebra k G and x,y,z ∈ G with H: ∀ a, a·x = z ↔ a = y, the coefficient (f * single x r).coeff z equals f.coeff y · y • r.

Русский

Пусть f ∈ SkewMonoidAlgebra k G и x,y,z ∈ G, с условием H: ∀ a, a·x = z ↔ a = y. Тогда (f * single x r).coeff z = f.coeff y · y • r.

LaTeX

$$$ (f * \mathrm{single}\; x\; r).\mathrm{coeff}(z) = f_{y} \; y \!\cdot r \quad\text{при } H: \forall a, a x = z \iff a = y $$$

Lean4

theorem coeff_mul_single_one (f : SkewMonoidAlgebra k G) (r : k) (x : G) :
    (f * single 1 r).coeff x = f.coeff x * x • r :=
  f.coeff_mul_single_aux fun a ↦ by rw [mul_one]

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