Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-07 23:27 a5b0376c

View on Github →

chore(topology/algebra/monoid,group): rename variables (#4516) Use M, N for monoids, G, H for groups.

Estimated changes

modified theorem compact_open_separated_mul
modified theorem continuous.inv
modified theorem continuous.sub
modified theorem continuous_at.inv
modified theorem continuous_inv
modified theorem continuous_on.inv
modified theorem continuous_on.sub
modified theorem continuous_on_inv
modified theorem continuous_sub
modified theorem continuous_within_at.inv
modified theorem exists_nhds_split4
modified theorem exists_nhds_split
modified theorem exists_nhds_split_inv
modified theorem filter.tendsto.inv
modified theorem filter.tendsto.sub
modified theorem is_closed_map_mul_left
modified theorem is_closed_map_mul_right
modified theorem is_open_map_mul_left
modified theorem is_open_map_mul_right
modified theorem is_open_mul_left
modified theorem is_open_mul_right
modified theorem nhds_is_mul_hom
modified theorem nhds_mul
modified theorem nhds_one_symm
modified theorem nhds_translation
modified theorem nhds_translation_mul_inv
modified theorem one_open_separated_mul
modified theorem quotient_group.open_coe
modified theorem quotient_group_saturate
modified theorem tendsto_inv
modified theorem topological_group.t1_space
modified theorem topological_group.t2_space
modified theorem continuous.mul
modified theorem continuous.pow
modified theorem continuous_at.mul
modified theorem continuous_finset_prod
modified theorem continuous_list_prod
modified theorem continuous_mul
modified theorem continuous_mul_left
modified theorem continuous_mul_right
modified theorem continuous_multiset_prod
modified theorem continuous_on.mul
modified theorem continuous_pow
modified theorem continuous_within_at.mul
modified theorem filter.tendsto.mul
modified theorem submonoid.mem_nhds_one
modified theorem tendsto_finset_prod
modified theorem tendsto_list_prod
modified theorem tendsto_mul
modified theorem tendsto_multiset_prod