coeff_mul_single_of_not_exists_mul

English

If there is no d ∈ G with g' = g d, then (x * single g r).coeff g' = 0 for any x ∈ SkewMonoidAlgebra k G.

Русский

Если не существует d ∈ G с g' = g d, то (x * single g r).coeff g' = 0 для любого x ∈ SkewMonoidAlgebra k G.

LaTeX

$$$\text{If } \nexists d,\ g' = g d, \text{ then } (x * \mathrm{single}\; g\; r).\mathrm{coeff}(g') = 0$$$

Lean4

theorem coeff_mul_single_of_not_exists_mul (r : k) {g g' : G} (x : SkewMonoidAlgebra k G) (h : ∀ x, ¬g' = x * g) :
    (x * single g r).coeff g' = 0 := by
  classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ rfl)

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