modOf_apply_of_exists_add — Mathlib

English

If there exists d with g' = g + d, then the coefficient of modOf g at g' is zero.

Русский

Если существует d такое, что g' = g + d, то коэффициент modOf g в g' равен нулю.

LaTeX

$$$\\bigl\\{ \\exists d, g' = g + d \\bigr\\} \\Rightarrow (x \\bmod^{\\circ} g)_{g'} = 0$$$

Lean4

@[simp]
theorem modOf_apply_of_exists_add (x : k[G]) (g : G) (g' : G) (h : ∃ d, g' = g + d) : (x %ᵒᶠ g) g' = 0 := by
  classical exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

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