inv_apply_self — Mathlib

English

For any e ∈ MulAut M and m ∈ M, e^{-1}(e(m)) = m, i.e. the inverse automorphism undoes the action of e.

Русский

Для любого e ∈ MulAut M и m ∈ M верно, что e^{-1}(e(m)) = m, то есть обратный автоморфизм отменяет действие e.

LaTeX

$$$ \forall e \in \mathrm{MulAut}(M), \forall m \in M,\; e^{-1}(e(m)) = m $$$

Lean4

theorem inv_apply_self (e : MulAut M) (m : M) : e⁻¹ (e m) = m :=
  MulEquiv.apply_symm_apply _ _

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