Mathlib v3 is deprecated. Go to Mathlib v4

Def bilin_form.dual_prod

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_prodView on Github →