Commit 2023-02-14 14:45 f69c5e4b

View on Github →

feat: port Topology.Algebra.Monoid (#2245)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Monoid.lean

added theorem Continuous.mul

added theorem Continuous.pow

added theorem Continuous.units_map

added theorem ContinuousAt.mul

added theorem ContinuousAt.pow

added theorem ContinuousMul.of_nhds_one

added theorem ContinuousOn.mul

added theorem ContinuousOn.pow

added theorem ContinuousWithinAt.mul

added theorem ContinuousWithinAt.pow

added theorem Filter.Tendsto.const_mul

added theorem Filter.Tendsto.mul

added theorem Filter.Tendsto.mul_const

added theorem Filter.Tendsto.pow

added def Filter.Tendsto.units

added theorem Filter.TendstoNhdsWithinIio.const_mul

added theorem Filter.TendstoNhdsWithinIio.mul_const

added theorem Filter.TendstoNhdsWithinIoi.const_mul

added theorem Filter.TendstoNhdsWithinIoi.mul_const

added theorem Filter.tendsto_cocompact_mul_left

added theorem Filter.tendsto_cocompact_mul_right

added theorem Inducing.continuousMul

added theorem IsCompact.mul

added theorem LocallyFinite.exists_finset_mulSupport

added theorem MonoidHom.isClosed_range_coe

added theorem Submonoid.coe_topologicalClosure

added def Submonoid.commMonoidTopologicalClosure

added theorem Submonoid.isClosed_topologicalClosure

added theorem Submonoid.le_topologicalClosure

added theorem Submonoid.mem_nhds_one

added theorem Submonoid.top_closure_mul_self_eq

added theorem Submonoid.top_closure_mul_self_subset

added def Submonoid.topologicalClosure

added theorem Submonoid.topologicalClosure_minimal

added theorem continuousAt_pow

added theorem continuousMul_induced

added theorem continuousMul_inf

added theorem continuousMul_infᵢ

added theorem continuousMul_infₛ

added theorem continuousMul_of_comm_of_nhds_one

added theorem continuousOn_finset_prod

added theorem continuousOn_list_prod

added theorem continuousOn_multiset_prod

added theorem continuousOn_pow

added theorem continuous_finprod

added theorem continuous_finprod_cond

added theorem continuous_finset_prod

added theorem continuous_list_prod

added theorem continuous_mul

added theorem continuous_mul_left

added theorem continuous_mul_right

added theorem continuous_multiset_prod

added theorem continuous_one

added theorem continuous_pow

added theorem eventuallyEq_prod

added theorem exists_nhds_one_split4

added theorem exists_nhds_one_split

added theorem exists_open_nhds_one_mul_subset

added theorem exists_open_nhds_one_split

added theorem finprod_eventually_eq_prod

added theorem isClosed_setOf_map_mul

added theorem isClosed_setOf_map_one

added theorem le_nhds_mul

added def monoidHomOfMemClosureRangeCoe

added def monoidHomOfTendsto

added theorem nhds_mul_nhds_one

added theorem nhds_one_mul_nhds

added theorem tendsto_finset_prod

added theorem tendsto_list_prod

added theorem tendsto_mul

added theorem tendsto_multiset_prod