Theorem IsSemitopologicalSemiring.continuousNeg_of_mul

Modification history

2026-03-26 18:37
Mathlib/Topology/Algebra/Ring/Basic.lean
feat: add `IsSemitopologicalRing` (#36617) …
Added IsSemitopologicalSemiring.continuousNeg_of_mulView on Github →