mem_inv_pointwise_smul_iff — Mathlib

English

Let K be a field with an action of a group G and S a valuation subring of K. Then for every g in G and x in K, x lies in g^{-1} · S if and only if g · x lies in S.

Русский

Пусть K — поле, на которое действует группа G, и S — подкольцо оценки K. Тогда для любого g∈G и любого x∈K верно: x ∈ g^{-1} · S тогда и только тогда, когда g · x ∈ S.

LaTeX

$$$ x \in g^{-1} \cdot S \leftrightarrow g \cdot x \in S $$$

Lean4

theorem mem_inv_pointwise_smul_iff {g : G} {S : ValuationSubring K} {x : K} : x ∈ g⁻¹ • S ↔ g • x ∈ S :=
  Set.mem_inv_smul_set_iff

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