There seems to be broad agreement that in the long term structure BilinForm should not exist - instead we should use M →ₗ[R] M →ₗ[R] R.

Many BilinForm results already have equivalents e.g. following #9485, many of the results in LinearAlgebra/Matrix/BilinearForm are just wrappers around results in LinearAlgebra/Matrix/SesquilinearForm.

One possible objection to removing BilinForm altogether at this stage is that it supports non-commutative semirings, which M →ₗ[R] M →ₗ[R] R does not support without further assumptions.

Zulip discussion:

• https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Quadratic.20Maps/near/395767687
• https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60bilinear_form.60

Related issues/PRs:

• [Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic): remove non-commutativity support #7581
• [Merged by Bors] - refactor(LinearAlgebra/Matrix/BilinearForm): Derive BilinearForm results from SesquilinearForm #9485
• [Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic): Use bilinear maps for the companion #10097
• [Merged by Bors] - refactor(LinearAlgebra/QuadraticForm): Replace BilinForm with a scalar valued bi LinearMap #10238
• refactor(LinearAlgebra/BilinearForm/Properties): Restrict the definition of BilinForm.IsSymm to commutative semiring #10422
• Create BilinearMap abbreviation #10424
• [Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Properties): Redefine BilinForm.IsRefl, BilinForm.IsAlt and BilinForm.IsSymm in terms of LinearMap equivalents  #10432
• refactor(LinearAlgebra/SesquilinearForm/Properties): Refactor BilinForm dual and nondegenerate properties #11032
• refactor(RingTheory/Trace): Define TraceForm with LinearMap.BilinForm #11057
• [Merged by Bors] - refactor(Algebra/Lie/SkewAdjoint): from BilinForm to LinearMap.BilinForm #11078
• Refactor bilinear forms mathlib3#15907