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 _ _⟩