smul_toBilin — Mathlib

English

For a scalar s in S, (s • Q).toBilin bm = s • (Q.toBilin bm). This says the operation of smul commutes with the bilinearization along the basis.

Русский

Для скаляра s ∈ S выполняется (s • Q).toBilin bm = s • (Q.toBilin bm). Это утверждает совместимость операции умножения на скаляры с билинейизацией по базису.

LaTeX

$$$ (s \\cdot Q)^{\\toBilin}_{bm} = s \\cdot (Q^{\\toBilin}_{bm}) $$$

Lean4

@[simp]
theorem smul_toBilin (bm : Basis ι R M) (s : S) (Q : QuadraticMap R M N) : (s • Q).toBilin bm = s • Q.toBilin bm :=
  by
  refine bm.ext fun i => bm.ext fun j => ?_
  obtain h | rfl | h := lt_trichotomy i j
  · simp [h.ne, h, toBilin_apply, polar_smul]
  · simp [toBilin_apply]
  · simp [h.ne', h.not_gt, toBilin_apply]

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