This repository was archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 292
Refactor bilinear forms #15907
Copy link
Copy link
Open
Labels
RFCRequest for commentRequest for commentt-algebraAlgebra (groups, rings, fields etc)Algebra (groups, rings, fields etc)
Description
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:
- [Merged by Bors] - feat(linear_algebra/matrix): Add matrix properties for sesquilinear forms #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
- [Merged by Bors] - chore(analysis/inner_product_space/basic): remove
bilin_form_of_real_inner#15780 - Remove
linear_algebra/matrix/bilinear_form.lean - Move remaining lemmas from
linear_algebra/bilinear_formtolinear_algebra/sesquilinear_formand deletelinear_algebra/bilinear_form - (optional/up for debate): rename
*/sesquilinear_formto*/bilinear_form
Metadata
Metadata
Assignees
Labels
RFCRequest for commentRequest for commentt-algebraAlgebra (groups, rings, fields etc)Algebra (groups, rings, fields etc)