pointwise_isCentralScalar — Mathlib

English

For ha ≠ 0, x ∈ a⁻¹ • S iff a • x ∈ S.

Русский

Пусть ha ≠ 0. Тогда x ∈ a⁻¹ • S ⇔ a • x ∈ S.

LaTeX

$$$ (ha \\neq 0) \\Rightarrow (x \\in a^{-1} \\cdot S \\iff a \\cdot x \\in S)$$$

Lean4

instance pointwise_isCentralScalar [DistribMulAction Mᵐᵒᵖ A] [IsCentralScalar M A] :
    IsCentralScalar M (AddSubgroup A) :=
  ⟨fun _ S => (congr_arg fun f => S.map f) <| AddMonoidHom.ext <| op_smul_eq_smul _⟩
    -- TODO: Check that these lemmas are useful and uncomment.
    -- @[simp]
    -- lemma smul_bot (m : M) : m • (⊥ : AddSubgroup A) = ⊥ := map_bot _

    -- lemma smul_sup (m : M) (S T : AddSubgroup A) : m • (S ⊔ T) = m • S ⊔ m • T := map_sup _ _ _

    -- @[simp]
    -- lemma smul_closure (m : M) (s : Set A) : m • closure s = closure (m • s) :=
    --   AddMonoidHom.map_closure ..

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