apply — Mathlib

English

Let Q1 and Q2 be quadratic maps on M1 and M2 over a commutative semiring R, and f an isometry from Q1 to Q2. Then the projection to the underlying domain maps yields a linear map f: M1 → M2; i.e., the isometry is determined by its action on M1.

Русский

Пусть Q1 и Q2 — квадратичные формы на модулях M1 и M2 над коммутативным полем R, и f — изометрия Q1 →qᵢ Q2. Тогда отображение 'apply' дает линейное отображение f: M1 → M2; изометрия определяется своим действием на M1.

LaTeX

$$$\mathrm{apply}(f) = f : M_1 \to M_2$$$

Lean4

/-- See Note [custom simps projection]. -/
protected def apply (f : Q₁ →qᵢ Q₂) : M₁ → M₂ :=
  f

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