mathlib

c2528003 - chore(*): use notation for `filter.prod` (#3768)

chore(*): use notation for `filter.prod` (#3768) Also change from `∀ v w ∈ V` to `∀ (v ∈ V) (w ∈ V)` in `exists_nhds_split_inv`, `exists_nhds_half_neg`, `add_group_with_zero_nhd.exists_Z_half`.