Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.eq_top_of_nonempty_interior'

Modification history

2021-08-22 16:54
src/topology/algebra/module.lean
feat(topology/basic): interior of a singleton (#8784) …
Modified submodule.eq_top_of_nonempty_interior'View on Github →
2020-07-21 01:55
src/topology/algebra/module.lean
refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481)
Added submodule.eq_top_of_nonempty_interior'View on Github →
2020-07-19 21:18
src/topology/algebra/module.lean
refactor(order/filter/basic): add class `filter.ne_bot` (#3454) …
Deleted submodule.eq_top_of_nonempty_interior'View on Github →
2020-02-19 21:46
src/topology/algebra/module.lean
refactor(analysis/calculus/tangent_cone): split a proof into parts (#2013) …
Added submodule.eq_top_of_nonempty_interior'View on Github →