support_divOf — Mathlib

English

The support of x.divOf g is the preimage under a + g of the support of x restricted to the injective domain.

Русский

Опора x.divOf g равна образу подмножества опоры x через добавление g с инъективностью.

LaTeX

$$$$\operatorname{supp}(x/divOf g) = \operatorname{supp}(x)^{g+·}$$$$

Lean4

@[simp]
theorem support_divOf (g : G) (x : k[G]) :
    (x /ᵒᶠ g).support = x.support.preimage (g + ·) (Function.Injective.injOn (add_right_injective g)) :=
  rfl

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