pointwiseMulAction — Mathlib

English

For any S ⊆ A and a ∈ Group G, x ∈ a⁻¹ • S iff a • x ∈ S.

Русский

Для любого подмножества S ⊆ A и любого a ∈ G: x ∈ a⁻¹ • S эквивалентно a • x ∈ S.

LaTeX

$$$ x \in a^{-1} \cdot S \iff a \cdot x \in S $$$

Lean4

/-- The action on an additive submonoid corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction M (AddSubmonoid A)
    where
  smul a S := S.map (DistribMulAction.toAddMonoidEnd _ A a)
  one_smul S := (congr_arg (fun f : AddMonoid.End A => S.map f) (MonoidHom.map_one _)).trans S.map_id
  mul_smul _ _
    S := (congr_arg (fun f : AddMonoid.End A => S.map f) (MonoidHom.map_mul _ _ _)).trans (S.map_map _ _).symm

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