ext_iff_of_isSymm — Mathlib

English

Two symmetric bilinear forms that agree on the diagonal are equal.

Русский

Две симметричные билинейные формы, совпадающие на диагонали, равны.

LaTeX

$$B.IsSymm → C.IsSymm → (∀ x, B x x = C x x) → B = C$$

Lean4

/-- A symmetric bilinear form is characterized by the values it takes on the diagonal. -/
theorem ext_iff_of_isSymm (hB : IsSymm B) (hC : IsSymm C) : B = C ↔ ∀ x, B x x = C x x
    where
  mp h := by simp [h]
  mpr := ext_of_isSymm hB hC

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