v_sq_scalar — Mathlib

English

For any m ∈ M, the product v(Q) m · v(Q) m equals the base-field image of the quadratic form: v(Q) m · v(Q) m = algebraMap_R^Cl(Q)(Q(m)).

Русский

Для любого m ∈ M произведение v(Q) m · v(Q) m равно образу квадратичной формы в базовой области: v(Q) m · v(Q) m = algebraMap_R^Cl(Q)(Q(m)).

LaTeX

$$$v_Q(m)\,v_Q(m) = \mathrm{algebraMap}_{R \to \mathrm{Cl}(Q)}(Q(m))$$$

Lean4

theorem v_sq_scalar (m : M) : v Q m * v Q m = algebraMap _ _ (Q m) :=
  (ι_sq_scalar _ _).trans <| by simp

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