Witt's Cancellation

Stream: maths

[Andy Heald]

I just spent a possibly inordinate amount of time convincing lean of the truth of the version of Witt's Cancellation Theorem found in Gersten's "Basic Quadratic Forms", i.e. that if two subspaces of a quadratic space are isometric, so are their orthogonal complements.

I suspect a lot of what I have done is incredibly non-optimal, but if anyone is interested in seeing what I've done let me know. Or conversely if it's already in MathLib under some name I couldn't ascertain.

[Johan Commelin]

Nice! I'm quite sure we don't have this yet, right @Eric Wieser ?

[Eric Wieser]

It's quite possible we have this for inner product spaces, but not general quadratic spaces

[Eric Wieser]

Which is to say: definitely add this to mathlib!