Commit 2026-08-12 20:57 93d2be25

refactor(LinearAlgebra/Orientation,LinearAlgebra/AffineSpace/FiniteDimensional): instances for arbitrary orientations (#39696) Based on suggestions by @kim-em on Zulip https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/PRs.20towards.20IMO.20geometry.202024.20P4/near/596946072 add convenience scoped instances for choosing an arbitrary orientation of a module, and for the finrank of the span of the vertices of a simplex. Note: I don't understand why the latter scoped instance is only found automatically in one of the two places using it; in Sphere/Power.lean it's necessary to use Affine.Simplex.fact_finrank_direction_affineSpan_eq rather than relying on typeclass inference, but in Angle/Sphere.lean typeclass inference suffices.