Theorems · Theorem · linear algebra

LinearMap.BilinForm.ext_of_isSymm

∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_8} [inst_1 : Field R] [NeZero 2] [inst_3 : Module R M]
  {B C : LinearMap.BilinForm R M}, B.IsSymm → C.IsSymm → (∀ (x : M), (B x) x = (C x) x) → B = C

A symmetric bilinear form is characterized by the values it takes on the diagonal.

Defined in

Mathlib.LinearAlgebra.BilinearForm.Properties

Cited by

3 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidFieldNeZeroModule