of'_mul_modOf — Mathlib

English

Multiplying a basis element by x and reducing modulo g yields zero after the reduction.

Русский

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

LaTeX

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

Lean4

theorem of'_mul_modOf (g : G) (x : k[G]) : of' k G g * x %ᵒᶠ 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, single_mul_apply_of_not_exists_add _ _ h]

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