I just open this to track my progress and let everyone know how I plan to do this. This is very tedious, so if anyone wants to help I would be really happy.
The goal is to completely remove bilin_form R M in favor of M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R, which is more general and this removes quite a few boilerplate lemmas since we can apply lemmas from linear_map.
The issue with this refactor is that bilin_form has a few dependencies and moving the lemmas is not trivial (even without the generalization), so doing everything in one PR is not feasible.
The roadmap is as follows:
I just open this to track my progress and let everyone know how I plan to do this. This is very tedious, so if anyone wants to help I would be really happy.
The goal is to completely remove
bilin_form R Min favor ofM₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R, which is more general and this removes quite a few boilerplate lemmas since we can apply lemmas fromlinear_map.The issue with this refactor is that
bilin_formhas a few dependencies and moving the lemmas is not trivial (even without the generalization), so doing everything in one PR is not feasible.The roadmap is as follows:
M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] Rbilin_form_of_real_inner#15780linear_algebra/matrix/bilinear_form.leanlinear_algebra/bilinear_formtolinear_algebra/sesquilinear_formand deletelinear_algebra/bilinear_form*/sesquilinear_formto*/bilinear_form