choose_exists_companion — Mathlib

English

In a ring, the companion bilinear form is unique and equals polarBilin Q.

Русский

В кольце компаньонная билинейная форма уникальна и равна polarBilin Q.

LaTeX

$$choose_exists_companion$$

Lean4

/-- In a ring the companion bilinear form is unique and equal to `QuadraticMap.polar`. -/
theorem choose_exists_companion : Q.exists_companion.choose = polarBilin Q :=
  LinearMap.ext₂ fun x y => by
    rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub, add_sub_cancel_left]

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