refactor(LinearAlgebra/BilinearForm/Basic): Deprecate

[mans0954]

Deprecate most of LinearAlgebra/BilinearForm/Basic.

---

[eric-wieser]

I'd argue that a lot of these might be worth keeping; the ₂ naming is a little odd if you're working with bilinear forms.

The coe lemmas are not, as their statement is nonsense after the last PR.

[mans0954]

I'd argue that a lot of these might be worth keeping; the ₂ naming is a little odd if you're working with bilinear forms.

I did wonder about that. We've ended up with some things in LinearMap.BilinForm and some things with the ₂ convention.

I suspect a lot of these things should be LinearMap.BilinMap or even LinearMap.SesquiMap so neither of the current naming conventions may be the final form?

[eric-wieser]

I suspect a lot of these things should be LinearMap.BilinMap or even LinearMap.SesquiMap so neither of the current naming conventions may be the final form?

I would be inclined not to deprecate these until we have a clearer picture of the final form. Perhaps let's create a new PR that deprecates just the nonsense coe lemmas, and leave the this PR until your BilinMap stuff lands?

[mans0954]

I would be inclined not to deprecate these until we have a clearer picture of the final form. Perhaps let's create a new PR that deprecates just the nonsense coe lemmas, and leave the this PR until your BilinMap stuff lands?

Okay, what about the _apply theorems?

[eric-wieser]

The apply theorems are good and we should keep them.

[mans0954]

Perhaps let's create a new PR that deprecates just the nonsense coe lemmas

#12132

[mans0954]

I'm going to close this PR for now in favour of:

• [Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Basic): Delete infered instances #12122
• [Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Basic): Derive the *_left and *_right results from the map_*₂ and map_* results #12124
• [Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Basic): Deprecate coercions #12132