English
The action of G on valuation subrings is order-preserving: if S1 ⊆ S2 then g•S1 ⊆ g•S2 for all g in G.
Русский
Действие группы G на ценностные подкольца сохраняет порядок: если S1 ⊆ S2, то g•S1 ⊆ g•S2 для любого g ∈ G.
LaTeX
$$For all g∈G and S1,S2, S1 ⊆ S2 ⇒ g•S1 ⊆ g•S2$$
Lean4
/-- The action on a valuation subring corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
def pointwiseHasSMul : SMul G (ValuationSubring K) where
smul g
S := -- TODO: if we add `ValuationSubring.map` at a later date, we should use it here
{ g • S.toSubring with
mem_or_inv_mem' := fun x =>
(mem_or_inv_mem S (g⁻¹ • x)).imp Subring.mem_pointwise_smul_iff_inv_smul_mem.mpr fun h =>
Subring.mem_pointwise_smul_iff_inv_smul_mem.mpr <| by rwa [smul_inv''] }
