Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-19 09:57 040ebea0

View on Github →

fix(analysis/normed_space/normed_group_quotient): put lemmas inside namespace (#7653)

Estimated changes

Modified src/analysis/normed_space/normed_group_quotient.lean

deleted theorem add_subgroup.is_quotient.norm_le

deleted theorem add_subgroup.is_quotient.norm_lift

deleted structure add_subgroup.is_quotient

deleted theorem add_subgroup.is_quotient_quotient

deleted def add_subgroup.lift

deleted theorem add_subgroup.lift_mk

deleted theorem add_subgroup.lift_unique

added theorem normed_group_hom.is_quotient.norm_le

added theorem normed_group_hom.is_quotient.norm_lift

added structure normed_group_hom.is_quotient

added theorem normed_group_hom.is_quotient_quotient

added def normed_group_hom.lift

added theorem normed_group_hom.lift_mk

added theorem normed_group_hom.lift_unique