ofIso_refl — Mathlib

English

The isomorphism constructed from the identity isometry is the identity isomorphism in QuadraticModuleCat.

Русский

Изоморфизм, полученный от тождевой изометрии, является тождевым изоморфизмом в QuadraticModuleCat.

LaTeX

$$$\\mathrm{ofIso}(\\mathrm{IsometryEquiv.refl}\\ Q_1) = \\mathrm{Iso}.refl (\\mathrm{of}\\ Q_1)$$$

Lean4

@[simp]
theorem ofIso_refl : ofIso (IsometryEquiv.refl Q₁) = .refl _ :=
  rfl

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