Commit 2022-01-14 10:07 021baaee

View on Github →

feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class (#11434) This also registers linear_isometry and linear_isometry_equiv with add_monoid_hom_class. I found myself wanting one of these while squeezing a simp, so may as well have all of them now.

Estimated changes

Modified src/analysis/complex/isometry.lean

deleted theorem linear_isometry_equiv.congr_fun

Modified src/analysis/normed_space/linear_isometry.lean

deleted theorem linear_isometry.coe_fn_injective

added theorem linear_isometry.coe_injective

added theorem linear_isometry.to_continuous_linear_map_inj

added theorem linear_isometry.to_continuous_linear_map_injective

added theorem linear_isometry.to_linear_map_inj

added theorem linear_isometry_equiv.coe_injective

added theorem linear_isometry_equiv.to_continuous_linear_equiv_inj

added theorem linear_isometry_equiv.to_continuous_linear_equiv_injective

added theorem linear_isometry_equiv.to_homeomorph_inj

added theorem linear_isometry_equiv.to_homeomorph_injective

added theorem linear_isometry_equiv.to_isometric_inj

added theorem linear_isometry_equiv.to_isometric_injective

added theorem linear_isometry_equiv.to_linear_equiv_inj

added theorem linear_isometry_equiv.to_linear_isometry_inj

added theorem linear_isometry_equiv.to_linear_isometry_injective