Matrix version of symmetric characterization

Stream: Is there code for X?

[Elif Uskuplu]

In Mathlib.LinearAlgebra.BilinearForm.Properties we have

theorem LinearMap.BilinForm.ext_of_isSymm
{M : Type u_2} [AddCommMonoid M] {R : Type u_8} [Field R] [NeZero 2] [Module R M]
{B C : LinearMap.BilinForm R M} (hB : B.IsSymm) (hC : C.IsSymm)
(h : ∀ (x : M), (B x) x = (C x) x) : B = C

I need a different version of this result. If A and B are two symmetric matrices over a field char ≠ 2 and ∀ (x : m → α), x ⬝ᵥ A *ᵥ x = x ⬝ᵥ B *ᵥ x then A=B. Does such a thing exist in mathlib? I tried to formalize it myself but couldn't manage. Any help would be great.

[Kevin Buzzard]

I am surprised that the mathlib result doesn't let R be an arbitrary commutative ring and assume only that multiplication by 2 is invertible. For your result, why not prove that the bilinear forms associated to the matrices are equal first?

[Elif Uskuplu]

@Kevin Buzzard If I understand you correctly, I can use Matrix.toBilin'.injective where

def Matrix.toBilin'{R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :
Matrix n n R₁ ≃ₗ[R₁] LinearMap.BilinForm R₁ (n → R₁)

Is that right?

[Elif Uskuplu]

Thanks, the following worked:

theorem matrix_ext_of_isSymm {n : Type*} [Fintype n] [DecidableEq n]
    {R : Type*} [Field R] [NeZero (2 : R)]
    {A B : Matrix n n R}
    (hA : A.IsSymm) (hB : B.IsSymm)
    (h : ∀ x : n → R, x ⬝ᵥ A *ᵥ x = x ⬝ᵥ B *ᵥ x) :
    A = B := by
  apply Matrix.toBilin'.injective
  apply LinearMap.BilinForm.ext_of_isSymm
  · rw [@LinearMap.BilinForm.isSymm_def]
    intro x y
    simp only [Matrix.toBilin'_apply]
    calc ∑ i, ∑ j, x i * A i j * y j
        = ∑ i, ∑ j, x i * A j i * y j := by
          congr 1; ext i; congr 1; ext j; rw [hA.apply i j]
      _ = ∑ j, ∑ i, y j * A j i * x i := by
          rw [Finset.sum_comm]; congr 1; ext j; congr 1; ext i; ring
      _ = ∑ i, ∑ j, y i * A i j * x j := by rfl
  · rw [@LinearMap.BilinForm.isSymm_def]
    intro x y
    simp only [Matrix.toBilin'_apply]
    calc ∑ i, ∑ j, x i * B i j * y j
        = ∑ i, ∑ j, x i * B j i * y j := by
          congr 1; ext i; congr 1; ext j; rw [hB.apply i j]
      _ = ∑ j, ∑ i, y j * B j i * x i := by
          rw [Finset.sum_comm]; congr 1; ext j; congr 1; ext i; ring
      _ = ∑ i, ∑ j, y i * B i j * x j := by rfl
  · intro x
    simp only [Matrix.toBilin'_apply']
    exact h x