mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Refactor bilinear forms

Open mcdoll opened this issue 3 years ago • 0 comments

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:

  • [x] #15906
  • [ ] Move quadratic form to M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
  • [ ] Move bilin_form.is_skew_adjoint_bracket to new structure
  • [ ] Move algebra.trace_form to new structure
  • [x] #15780
  • [ ] Remove linear_algebra/matrix/bilinear_form.lean
  • [ ] Move remaining lemmas from linear_algebra/bilinear_form to linear_algebra/sesquilinear_form and delete linear_algebra/bilinear_form
  • [ ] (optional/up for debate): rename */sesquilinear_form to*/bilinear_form

mcdoll avatar Aug 07 '22 12:08 mcdoll