Theorem ContinuousInv₀.of_nhds_one

Modification history

2025-09-03 02:00
Mathlib/Topology/Algebra/GroupWithZero.lean
style: `HasContinuousInv₀` to `ContinuousInv₀` (#29201) …
Added ContinuousInv₀.of_nhds_oneView on Github →