Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quadratic_form.to_dual_prod_isometry

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 quadratic_form.to_dual_prod_isometryView on Github →