instSubsingleton — Mathlib

English

There is a zero map from any quadratic form Q1 to any Q2, i.e., a trivial isometry when the domain is mapped to zero.

Русский

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

LaTeX

$$$0 : (Q_1 \to qᵢ Q_2)$ is defined with zero linear map and map_app' := map_zero _$$

Lean4

/-- Maps into the zero module are trivial -/
instance [Subsingleton M₂] : Subsingleton (Q₁ →qᵢ Q₂) :=
  ⟨fun _ _ => ext fun _ => Subsingleton.elim _ _⟩

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