Theorem Filter.HasBasis.mul_self

Modification history

2025-01-28 07:32
Mathlib/Topology/Algebra/Monoid.lean
feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
Added Filter.HasBasis.mul_selfView on Github →