Commit 2025-12-19 15:37 b0ebf7a9

feat(Analysis/InnerProductSpace/PiL2): Add instances for EuclideanSpace rank and EuclideanSpace being infinite (#28198) Add an instance for Fact (Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n) which is needed to apply stereographic' to EuclideanSpace. Also add an instance for Infinite (EuclideanSpace 𝕜 ι) where ι is a nonempty fintype. I wasn't sure if these should go in separate pull requests, but they seemed similar enough to me. Thank you to Kenny Lau for the suggestions at #mathlib4 > Instances for EuclideanSpace.