Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.pointwise_mul_ne_empty

Modification history

2020-02-05 06:25
src/algebra/pointwise.lean
refactor(*): migrate from `≠ ∅` to `set.nonempty` (#1954) …
Deleted set.pointwise_mul_ne_emptyView on Github →
2019-07-18 15:15
src/algebra/pointwise.lean
feat(topology/algebra/group): define filter pointwise addition (#1215) …
Added set.pointwise_mul_ne_emptyView on Github →