Commit 2022-11-07 10:04 1f195436

View on Github →

feat(topology/algebra/group): • lemmas (#17383) Write the smul version of several mul lemmas, along with the missing instance has_continuous_mul M M → has_continuous_smul Mᵐᵒᵖ M

Estimated changes

Modified src/data/set/pointwise/basic.lean

added theorem set.bUnion_op_smul_set

Modified src/topology/algebra/const_mul_action.lean

Modified src/topology/algebra/group.lean

modified theorem is_open.mul_left

added theorem is_open.smul_left

added theorem subset_interior_mul'

added theorem subset_interior_smul

added theorem subset_interior_smul_right

modified theorem topological_space.positive_compacts.locally_compact_space_of_group

Modified src/topology/algebra/monoid.lean