English
The SemilinearIsometryEquivClass structure is preserved under the relevant constructions, giving a canonical instance of SemilinearIsometryClass from a SemilinearIsometryEquivClass.
Русский
Структура SemilinearIsometryEquivClass сохраняется под соответствующими конструкциями, образуя канонический элемент SemilinearIsometryClass из SemilinearIsometryEquivClass.
LaTeX
$$$\\text{instSemilinearIsometryEquivClass} : \\text{SemilinearIsometryEquivClass }(\\mathcal{L}, E, E') \\Rightarrow \\text{SemilinearIsometryClass }(\\mathcal{L}, E, E')$$$
Lean4
instance instEquivLike : EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂
where
coe e := e.toFun
inv e := e.invFun
coe_injective' f g h₁
h₂ := by
obtain ⟨f', _⟩ := f
obtain ⟨g', _⟩ := g
cases f'
cases g'
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, DFunLike.coe_fn_eq] at h₁
congr
left_inv e := e.left_inv
right_inv e := e.right_inv
