mathlib

1f00800d - feat(linear_algebra/projection) : projections are conjugate to prod_map id 0 (#13802)