instNeg — Mathlib

English

If Q: N → P is a quadratic map and f: M →ₗ[R] N is a linear map, then Q ∘ f is a quadratic map M → P defined by (Q ∘ f)(x) = Q(f(x)).

Русский

Если Q: N → P — квадратичная карта, а f: M → N — линейное отображение, то Q ∘ f является квадратичной картой M → P и задаётся через (Q ∘ f)(x) = Q(f(x)).

LaTeX

$$$ (Q \\circ f)(x) = Q(f(x)) $ for all x ∈ M.$$

Lean4

instance : Neg (QuadraticMap R M N) :=
  ⟨fun Q =>
    { toFun := -Q
      toFun_smul := fun a x => by simp only [Pi.neg_apply, Q.map_smul, smul_neg]
      exists_companion' :=
        let ⟨B, h⟩ := Q.exists_companion
        ⟨-B, fun x y => by simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]⟩ }⟩

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