refactor(LinearAlgebra/BilinearForm/Properties): Restrict the definition of BilinForm.IsSymm to commutative semiring

[mans0954]

Restrict the definition of BilinForm.IsSymm and BilinForm.IsRefl to modules over a commutative semiring.

Currently BilinForm.IsSymm and BilinForm.IsRefl are defined for modules over a semiring, whereas LinearMap.IsSymm is defined for modules over a commutative semiring. We wish to redefine BilinForm.IsSymm in terms of LinearMap.IsSymm as part of #10432. This PR is a preliminary step in that direction.

---

[adri326]

This sounds like a strict downgrade: the definition of BilinForm.IsSymm doesn't use the commutative property, and LinearMap doesn't require a commutative semiring, so why restrict it?

[Vierkantor]

This sounds like a strict downgrade: the definition of BilinForm.IsSymm doesn't use the commutative property, and LinearMap doesn't require a commutative semiring, so why restrict it?

Linear maps don't, but bilinear maps do, since the instance Module R (M₂ →ₛₗ[I₂] M) does (or to be more precise, we need SMulCommClass R R M), to show that map_smul holds: a • f (c • x) = c • a • f x. See also this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60

[Vierkantor]

I think replacing BilinearForm with a bilinear map is the way to go, since the bilinear condition in the non-commutative setting is not very useful anyway. But this approach seems fragile and too much work. If the commutativity will be required in the end anyway, why not make a PR that replaces the [Semiring] and [Ring] assumptions with [CommSemiring] and [CommRing] everywhere in the LinearAlgebra/Bilinear/ folder?

[Vierkantor]

I made a start in commit 4244c22, and it builds. We still need to deduplicate/rename the variables in those files. Feel free to adopt.

[eric-wieser]

I attempted to resolve the conflicts, it seems that #11280 completely subsumed this.