Commit 2021-08-09 15:47 3ec899aa

View on Github →

chore(topology/algebra): bundled homs in group and ring completion (#8497) Also take the opportunity to remove is_Z_bilin (who was scheduled for removal from the beginning).

Estimated changes

Modified src/topology/algebra/group_completion.lean

added def add_monoid_hom.completion

added theorem add_monoid_hom.completion_add

added theorem add_monoid_hom.completion_coe

added theorem add_monoid_hom.completion_zero

added theorem add_monoid_hom.continuous_completion

added theorem add_monoid_hom.continuous_extension

added def add_monoid_hom.extension

added theorem add_monoid_hom.extension_coe

added theorem uniform_space.completion.continuous_to_compl

deleted theorem uniform_space.completion.is_add_group_hom_coe

deleted theorem uniform_space.completion.is_add_group_hom_extension

deleted theorem uniform_space.completion.is_add_group_hom_map

added def uniform_space.completion.to_compl

Modified src/topology/algebra/uniform_group.lean

deleted theorem add_comm_group.is_Z_bilin.comp_hom

deleted theorem add_comm_group.is_Z_bilin.neg_left

deleted theorem add_comm_group.is_Z_bilin.neg_right

deleted theorem add_comm_group.is_Z_bilin.sub_left

deleted theorem add_comm_group.is_Z_bilin.sub_right

deleted theorem add_comm_group.is_Z_bilin.zero

deleted theorem add_comm_group.is_Z_bilin.zero_left

deleted theorem add_comm_group.is_Z_bilin.zero_right

modified theorem dense_inducing.extend_Z_bilin

deleted theorem is_Z_bilin.tendsto_zero_left

deleted theorem is_Z_bilin.tendsto_zero_right

Modified src/topology/algebra/uniform_ring.lean

added theorem uniform_space.completion.continuous_coe_ring_hom

modified def uniform_space.completion.map_ring_hom