Commit 2026-05-16 09:43 146974d9

View on Github →

chore: rename Linear.smulRight_eq_comp (#39360) The current name is misleading (the lemma is about alternating maps, not mere linear maps), and will lead to a name conflict when a version for symmetric maps is added. Written at the ICERM workshop "Techniques and Tools for the Formalization of Analysis". From the project towards jet bundles.

Estimated changes