Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bilin_form.dual_prod.to_quadratic_form

Modification history

2023-07-26 13:39
src/linear_algebra/quadratic_form/dual.lean
feat(linear_algebra/quadratic_form): some work from 'Clifford Algebras and Spinor Norms Over a Commutative Ring' (#18447)
Added bilin_form.dual_prod.to_quadratic_formView on Github →