Commit 2020-02-19 21:46 5b77b64f

refactor(analysis/calculus/tangent_cone): split a proof into parts (#2013)

refactor(analysis/calculus/tangent_cone): split a proof into parts Prove submodule.eq_top_of_nonempty_interior and use it in the proof of unique_diff_on_convex.
Update src/analysis/normed_space/basic.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Fix a docstring.
Update src/topology/algebra/module.lean