mul_of'_modOf — Mathlib

English

Multiplication of x by the basis element and reduction by g yields zero remainder.

Русский

Умножение x на базисный элемент и редукция по g дают нулевой остаток.

LaTeX

$$$x \\cdot \\operatorname{of}'(g) \\bmod^{\\circ} g = 0$$$

Lean4

theorem mul_of'_modOf (x : k[G]) (g : G) : x * of' k G g %ᵒᶠ g = 0 :=
  by
  ext g'
  rw [Finsupp.zero_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  · rw [modOf_apply_self_add]
  · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]
    simpa only [add_comm] using h

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