Commit 2023-12-27 09:02 bbf5f350

View on Github →

chore(Topology/FilterBasis): rename GroupFilterBasis.prod_subset_self (#9233) ... to subset_mul_self

Estimated changes

Modified Mathlib/Topology/Algebra/FilterBasis.lean

deleted theorem GroupFilterBasis.prod_subset_self

added theorem GroupFilterBasis.subset_mul_self