Witt's Cancellation Theorem (continuation from Fall 2023)
Thm: Let ⟨-,-⟩ be a symmetric bilinear form (i.e. ⟨x,y⟩ = ⟨y,x⟩ for all x,y ∈ V). Suppose that
there is form-preserving map g: U → U' where U, U' ⊂ V are subspaces. Then there is a
form-preserving map f: V → V extending g.
Cor: U ⊕ V ≅ W ⊕ V ⟹ U ≅ W.
Members: Andy Heald, Nathan Louie, Sarah Mathison, Qiguang Yan
Formalizing Math 300 (continuation from Fall 2023)
Goal: Formalize the exercises (and possibly results) in the Math 300 textbook by Conroy--Taggart:
An Introduction to Mathematical Reasoning.
