Mathlib Changelog
v4
Changelog
About
Github
Def
OrthogonalFamily.decomposition
Modification history
2024-05-07 01:05
Mathlib/Analysis/InnerProductSpace/Projection.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted
OrthogonalFamily.decomposition
View on Github →
2023-06-14 02:02
Mathlib/Analysis/InnerProductSpace/Projection.lean
chore: forward-port leanprover-community/mathlib#14870 (#4699) …
Added
OrthogonalFamily.decomposition
View on Github →