equivOfIsometry_symm — Mathlib

English

The inverse of the algebra isomorphism corresponding to an isometry e equals the algebra isomorphism corresponding to e symm.

Русский

Обратный к алгебраическому изоморфизму, соответствующему изометрии e, равен изоморфизму, соответствующему e симм.

LaTeX

$$$ (\mathrm{equivOfIsometry} e).\mathrm{symm} = \mathrm{equivOfIsometry} (e).\mathrm{symm}. $$$

Lean4

@[simp]
theorem equivOfIsometry_symm (e : Q₁.IsometryEquiv Q₂) : (equivOfIsometry e).symm = equivOfIsometry e.symm :=
  rfl

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