Equivalent — Mathlib

English

There is an isometry between Q1 and Q2 whenever Q1 = Q2, given by identity on the common form.

Русский

Существует изометрия между Q1 и Q2, если Q1 = Q2, заданная как тождественная на общей форме.

LaTeX

$$$\mathrm{ofEq} : Q_1 = Q_2 \Rightarrow (Q_1 \to qᵢ Q_2)$$$

Lean4

/-- Two quadratic forms over a ring `R` are equivalent
if there exists an isometric equivalence between them:
a linear equivalence that transforms one quadratic form into the other. -/
def Equivalent (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) : Prop :=
  Nonempty (Q₁.IsometryEquiv Q₂)

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