mathlib
cb3c2b9e - fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750)

Commit

3 years ago

fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750) Without these the lemmas contain nonsense statements of the form `(x : α) ≤ (y : αᵒᵈ)`.

Author

eric-wieser

Parents

daac51e8

mathlib cb3c2b9e - fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750)

mathlib
cb3c2b9e - fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750)