English
Let M be a type equipped with a multiplication. For every multiplicative automorphism e of M and every m in M, the inverse of e acts on m the same way as the inverse automorphism, i.e. e^{-1}(m) = (e)^{-1}(m).
Русский
Пусть M — множество с умножением. Для каждой мультифицированной автоморфизмы e из MulAut(M) и каждого элемента m ∈ M верно, что e^{-1}(m) действует так же, как обратная автоморфизма: e^{-1}(m) = (e)^{-1}(m).
LaTeX
$$$ \forall e \in \mathrm{MulAut}(M), \forall m \in M,\; e^{-1}(m) = (e)^{-1}_{\text{symm}}(m) $$$
Lean4
@[simp]
theorem inv_apply (e : MulAut M) (m : M) : e⁻¹ m = e.symm m := by rw [inv_def]
