smul_apply — Mathlib

English

There is a natural SMul action of S on QuadraticMap R M N, given by (a • Q)(x) = a • (Q x) with corresponding bilinear companion transformed compatibly.

Русский

Существует естественное действие SMul на QuadaticMap: (a • Q)(x) = a • (Q x) с соответствующим преобразованием связанной билинейной формы.

LaTeX

$$$ (a\\,\\cdot\\, Q)(x) = a\\,\\cdot\\, (Q\\,x) \\,\\land\\, \\text{(companion maps scale compatibly)} $$$

Lean4

@[simp]
theorem smul_apply (a : S) (Q : QuadraticMap R M N) (x : M) : (a • Q) x = a • Q x :=
  rfl

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