Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_right_continuous

Modification history

2020-07-31 17:41
src/topology/algebra/ring.lean
feat(analysis/calculus/fderiv): inversion is differentiable (#3510) …
Added mul_right_continuousView on Github →