Commit 2025-04-03 18:02 99717f89
View on Github →feat(LinearAlgebra/Dual/Basis): Add two lemmas small about coords and dual bases (#23587)
This PR adds two small lemmas about how coordinates behave when moving to the dual space.
These aren't simp
lemmas since they are not in simp-normal form.