Commit 2023-04-06 07:51 2f266039

View on Github →

feat: port Topology.Algebra.FilterBasis (#3279)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/FilterBasis.lean

added theorem ContinuousSMul.of_basis_zero

added def GroupFilterBasis.N

added theorem GroupFilterBasis.N_one

added theorem GroupFilterBasis.conj

added theorem GroupFilterBasis.inv

added theorem GroupFilterBasis.mem_nhds_one

added theorem GroupFilterBasis.mul

added theorem GroupFilterBasis.nhds_eq

added theorem GroupFilterBasis.nhds_hasBasis

added theorem GroupFilterBasis.nhds_one_eq

added theorem GroupFilterBasis.nhds_one_hasBasis

added theorem GroupFilterBasis.one

added theorem GroupFilterBasis.prod_subset_self

added def GroupFilterBasis.topology

added def ModuleFilterBasis.ofBases

added theorem ModuleFilterBasis.smul

added theorem ModuleFilterBasis.smul_left

added theorem ModuleFilterBasis.smul_right

added def ModuleFilterBasis.topology'

added def ModuleFilterBasis.topology

added structure ModuleFilterBasis

added theorem RingFilterBasis.mul

added theorem RingFilterBasis.mul_left

added theorem RingFilterBasis.mul_right

added def RingFilterBasis.topology

added def groupFilterBasisOfComm