instZeroOfNat — Mathlib

English

If the codomain module M2 is a Subsingleton, then there is at most one isometry Q1 →qᵢ Q2.

Русский

Если кодомодуль M2 является Subsingleton, то существует не более одной изометрии Q1 →qᵢ Q2.

LaTeX

$$$\text{Subsingleton }M_2 \Rightarrow \text{Subsingleton}(Q_1 \to qᵢ Q_2)$$$

Lean4

/-- There is a zero map from any module with the zero form. -/
instance : Zero ((0 : QuadraticMap R M₁ N) →qᵢ Q₂) where
  zero := { (0 : M₁ →ₗ[R] M₂) with map_app' := fun _ => map_zero _ }

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