English
For f ∈ SkewMonoidAlgebra k G, x,y,z ∈ G and H: ∀ a, a·x = y ↔ a = z, we have (f * single x r).coeff y = f.coeff z · z • r.
Русский
Для f ∈ SkewMonoidAlgebra k G, x,y,z ∈ G и условие H: ∀ a, a·x = y ↔ a = z, верно (f * single x r).coeff y = f.coeff z · z • r.
LaTeX
$$$ (f * \mathrm{single}\; x\; r).\mathrm{coeff}(y) = f_{z} \; z \cdot r,\quad \text{при } \forall a, a x = y \iff a = z $$$
Lean4
theorem coeff_single_mul_aux (f : SkewMonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ a, x * a = y ↔ a = z) :
(single x r * f).coeff y = r * x • f.coeff z := by
classical
have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp
calc
((single x r) * f).coeff y = sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
(coeff_mul _ _ _).trans <| sum_single_index this
_ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
_ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
_ = _ := by split_ifs with h <;> simp [support] at h <;> simp [h]
