Commit 2023-12-17 20:09 f1ba2113

View on Github →

chore(LinearAlgebra/CliffordAlgebra): move results about inversion to a new file (#9075) I plan to contribute a few more of these, and this provides a better place for them to live. No lemma statements or proofs have changed. These were originally contributed in leanprover-community/mathlib#16077.

Estimated changes