Sesquilinear forms over a star ring

This file provides some properties about sesquilinear forms M →ₗ⋆[R] M →ₗ[R] R when R is a StarRing.

theorem LinearMap.isSymm_iff_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid M] [Module R M] {B : M →ₗ⋆[R] M →ₗ[R] R} {ι : Type u_4} (b : Module.Basis ι R M) : B.IsSymm ↔ ∀ (i j : ι), star ((B (b i)) (b j)) = (B (b j)) (b i)

theorem LinearMap.isSymm_iff_isHermitian_toMatrix {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M) : B.IsSymm ↔ ((toMatrix₂ b b) B).IsHermitian

theorem star_dotProduct_toMatrix₂_mulVec {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M) (x y : n → R) : star x ⬝ᵥ ((LinearMap.toMatrix₂ b b) B).mulVec y = (B (b.equivFun.symm x)) (b.equivFun.symm y)

theorem apply_eq_star_dotProduct_toMatrix₂_mulVec {R : Type u_1} {M : Type u_2} {n : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid M] [Module R M] [Fintype n] [DecidableEq n] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M) (x y : M) : (B x) y = star ⇑(b.repr x) ⬝ᵥ ((LinearMap.toMatrix₂ b b) B).mulVec ⇑(b.repr y)

theorem LinearMap.isPosSemidef_iff_posSemidef_toMatrix {M : Type u_2} {n : Type u_3} [AddCommMonoid M] [Fintype n] [DecidableEq n] {R : Type u_4} [CommRing R] [StarRing R] [PartialOrder R] [Module R M] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M) : B.IsPosSemidef ↔ ((toMatrix₂ b b) B).PosSemidef