smul — Mathlib

English

If m is a unit in the monoid M and g acts on M, then g • m is also a unit. In particular, the action by G preserves invertibility of elements of M.

Русский

Если m является единицей в моноиде M и G действует на M, то g • m также является единицей. Вторично, действие сохраняет обратимость элементов.

LaTeX

$$$\forall g \in G,\; (\text{IsUnit}(m) ) \Rightarrow (\text{IsUnit}(g \cdot m)).$$$

Lean4

@[to_additive]
theorem smul [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] {m : M} (g : G)
    (h : IsUnit m) : IsUnit (g • m) :=
  let ⟨u, hu⟩ := h
  hu ▸ ⟨g • u, Units.val_smul _ _⟩

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