Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 15:18 55b2e864

View on Github →

feat(analysis/normed_space): normed group hom completion (#8499) From LTE

Estimated changes

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem normed_group_hom.mem_range_self

added theorem normed_group_hom.surjective_on_with.exists_pos

added theorem normed_group_hom.surjective_on_with.mono

Created src/analysis/normed_space/normed_group_hom_completion.lean

added theorem normed_group.dense_range_to_compl

added theorem normed_group.norm_to_compl

added def normed_group.to_compl

added def normed_group_hom.completion

added theorem normed_group_hom.completion_add

added theorem normed_group_hom.completion_coe

added theorem normed_group_hom.completion_coe_to_fun

added theorem normed_group_hom.completion_comp

added theorem normed_group_hom.completion_def

added theorem normed_group_hom.completion_id

added theorem normed_group_hom.completion_neg

added theorem normed_group_hom.completion_sub

added theorem normed_group_hom.completion_to_compl

added theorem normed_group_hom.ker_completion

added theorem normed_group_hom.ker_le_ker_completion

added theorem normed_group_hom.norm_completion

added theorem normed_group_hom.zero_completion

added def normed_group_hom_completion_hom