English
If B and C are symmetric and they have equal diagonal values, then B = C.
Русский
Если B и C симметричны и их диагональные значения равны, то B = C.
LaTeX
$$B.IsSymm → C.IsSymm → (∀ x, B x x = C x x) → B = C$$
Lean4
theorem isSymm_iff_basis {ι : Type*} (b : Basis ι R M) : IsSymm B ↔ ∀ i j, B (b i) (b j) = B (b j) (b i)
where
mp := fun ⟨h⟩ i j ↦ h _ _
mpr := by
refine fun h ↦ ⟨fun x y ↦ ?_⟩
obtain ⟨fx, tx, ix, -, hx⟩ :=
Submodule.mem_span_iff_exists_finset_subset.1 (by simp : x ∈ Submodule.span R (Set.range b))
obtain ⟨fy, ty, iy, -, hy⟩ :=
Submodule.mem_span_iff_exists_finset_subset.1 (by simp : y ∈ Submodule.span R (Set.range b))
rw [← hx, ← hy]
simp only [map_sum, map_smul, coeFn_sum, Finset.sum_apply, smul_apply, smul_eq_mul, Finset.mul_sum]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)
rw [mul_left_comm]
obtain ⟨i, rfl⟩ := ix h₁
obtain ⟨j, rfl⟩ := iy h₂
rw [h]
