instEquivLike — Mathlib

English

The family of isometric equivalences between two quadratic forms forms an EquivLike structure, i.e., behaves like a set of linear equivalences with composition and inverse.

Русский

Множество изометрических эквивалентностей между квадратичными формами образует структуру EquivLike, ведующую себя как множество линейных эквивалентностей с операциями композиции и обрата.

LaTeX

$$$\text{IsometryEquiv}(Q_1,Q_2) \text{is equipped with an EquivLike structure}$$$

Lean4

instance : EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂
    where
  coe f := f.toLinearEquiv
  inv f := f.toLinearEquiv.symm
  left_inv f := f.toLinearEquiv.left_inv
  right_inv f := f.toLinearEquiv.right_inv
  coe_injective' f g := by cases f; cases g; simp +contextual

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