coroot_apply_self

Mathlib.LinearAlgebra.RootSystem.OfBilinear

URI: https://scilib.ai/kg/mathlib#LinearMap.IsReflective.coroot_apply_self

English

The coroot applied to x equals 2.

Русский

Корoot, применённый к x, равен 2.

LaTeX

$$coroot B hx x = 2$$

Lean4

@[simp]
theorem coroot_apply_self : coroot B hx x = 2 :=
  hx.regular.left <| by simp [mul_comm _ (B x x)]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru