mathlib3

8edffc25 - feat(order/filter/bases): lemmas about bases of product filters (#15630)

feat(order/filter/bases): lemmas about bases of product filters (#15630) * Move `has_basis.prod_self` and `mem_prod_self_iff` down to golf the proof. * Rename `has_basis.prod''` to `has_basis.prod_pprod`. * Rename `has_basis.prod'` to `has_basis.prod_same_index`. * Add `has_basis.prod_same_index_mono ` and `has_basis.prod_same_index_anti`.