Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-05-26 16:47
4ca776ee
View on Github →
feat(linear_algebra/quadratic_form): equivalence of quadratic forms (
#2769
)
Estimated changes
Modified
src/linear_algebra/quadratic_form.lean
added
theorem
quadratic_form.equivalent.refl
added
theorem
quadratic_form.equivalent.symm
added
theorem
quadratic_form.equivalent.trans
added
def
quadratic_form.equivalent
added
theorem
quadratic_form.isometry.map_app
added
def
quadratic_form.isometry.refl
added
def
quadratic_form.isometry.symm
added
def
quadratic_form.isometry.trans
added
structure
quadratic_form.isometry