Mathlib v3 is deprecated. Go to Mathlib v4

Def quadratic_form.dual_prod_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.dual_prod_prod_isometryView on Github →