Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-26 13:39 d11f435d

View on Github →

feat(linear_algebra/quadratic_form): some work from 'Clifford Algebras and Spinor Norms Over a Commutative Ring' (#18447)

Estimated changes

Modified docs/references.bib

Modified src/linear_algebra/quadratic_form/basic.lean

modified def quadratic_form.associated

Created src/linear_algebra/quadratic_form/dual.lean

added theorem bilin_form.dual_prod.to_quadratic_form

added def bilin_form.dual_prod

added theorem bilin_form.is_symm_dual_prod

added theorem bilin_form.nondenerate_dual_prod

added def quadratic_form.dual_prod

added def quadratic_form.dual_prod_isometry

added def quadratic_form.dual_prod_prod_isometry

added def quadratic_form.to_dual_prod

added theorem quadratic_form.to_dual_prod_isometry