Theorem nhds_inv₀

Modification history

2023-11-08 13:26
Mathlib/Topology/Algebra/GroupWithZero.lean
feat: add lemmas about `Inv.inv` for `Filter`s (#8261)
Added nhds_inv₀View on Github →