mathlib
c9b80414 - feat(linear_algebra/dual): more about `dual_annihilator` (#17313)

Commit

3 years ago

feat(linear_algebra/dual): more about `dual_annihilator` (#17313) Also gives `dual_annihilator_sup_eq_inf_dual_annihilator` a shorter name.

Author

kmill

Parents