ofIso_symm — Mathlib

English

For any isometry equivalence e between Q1 and Q2, the corresponding isomorphism in QuadraticModuleCat respects symmetry, i.e., value on symm is the inverse isometry.

Русский

Для любой изометрической эквиваленции e между Q1 и Q2 соответствующий изоморфизм в QuadraticModuleCat сохраняет симметрию: применённое к симметрии отображение равно обратному изоморфизму.

LaTeX

$$$\\mathrm{toIsometryEquiv}(e^{\\mathrm{symm}}) = (\\mathrm{toIsometryEquiv}(e))^{\\mathrm{symm}}$$$

Lean4

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

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