instZero — Mathlib

English

There exists a quadratic map that sends every element to zero; this zero map is additive and respects scalar action.

Русский

Существует квадратичная карта, отправляющая каждый вектор в 0; эта нулевая карта является аддитивной и корректно ведёт себя относительно действия скаляров.

LaTeX

$$$\\exists Q:\\ QuadraticMap(R,M,N)\\;\\forall x\\in M:\\; Q(x)=0.$$$

Lean4

instance : Zero (QuadraticMap R M N) :=
  ⟨{  toFun := fun _ => 0
      toFun_smul := fun a _ => by simp only [smul_zero]
      exists_companion' := ⟨0, fun _ _ => by simp only [add_zero, LinearMap.zero_apply]⟩ }⟩

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