smul_coroot — Mathlib

English

The scalar action of the coroot on x yields twice the bilinear form with x and y, as a function of y.

Русский

Скалярное действие корота на x даёт дважды значение билинейной формы на x и y.

LaTeX

$$B x x • coroot B hx y = 2 • B x y$$

Lean4

@[simp]
theorem smul_coroot : B x x • coroot B hx = 2 • B x := by
  ext y
  simp [smul_apply, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat, apply_self_mul_coroot_apply]

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