Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 18:34 a5fc0a33

View on Github →

feat(topology/algebra): filters bases for algebra (#9480) This is modernized version of code from the perfectoid spaces project.

Estimated changes

Modified src/algebra/pointwise.lean

added theorem set.mem_smul_of_mem

Modified src/order/filter/bases.lean

Created src/topology/algebra/filter_basis.lean

added def group_filter_basis.N

added theorem group_filter_basis.N_one

added theorem group_filter_basis.conj

added theorem group_filter_basis.inv

added theorem group_filter_basis.mem_nhds_one

added theorem group_filter_basis.mul

added theorem group_filter_basis.nhds_eq

added theorem group_filter_basis.nhds_has_basis

added theorem group_filter_basis.nhds_one_eq

added theorem group_filter_basis.nhds_one_has_basis

added theorem group_filter_basis.one

added theorem group_filter_basis.prod_subset_self

added def group_filter_basis.topology

added def group_filter_basis_of_comm

added def module_filter_basis.of_bases

added theorem module_filter_basis.smul

added theorem module_filter_basis.smul_left

added theorem module_filter_basis.smul_right

added def module_filter_basis.topology'

added def module_filter_basis.topology

added structure module_filter_basis

added theorem ring_filter_basis.mul

added theorem ring_filter_basis.mul_left

added theorem ring_filter_basis.mul_right

added def ring_filter_basis.topology

Modified src/topology/algebra/ring.lean

added theorem topological_ring.of_add_group_of_nhds_zero

added theorem topological_ring.of_nhds_zero