Commit 2020-04-26 09:29 40e97d37

View on Github →

feat(topology/algebra/module): ker, range, cod_restrict, subtype_val, coprod (#2525) Also move smul_right to general_ring and define some maps/equivalences useful for the inverse/implicit function theorem.

Estimated changes

Modified src/algebra/group/units.lean

added theorem units.coe_mk

Modified src/topology/algebra/module.lean

added def continuous_linear_equiv.equiv_of_inverse

added theorem continuous_linear_equiv.equiv_of_inverse_apply

added def continuous_linear_equiv.equiv_of_right_inverse

added theorem continuous_linear_equiv.equiv_of_right_inverse_symm_apply

added theorem continuous_linear_equiv.ext₁

added theorem continuous_linear_equiv.fst_equiv_of_right_inverse

added theorem continuous_linear_equiv.snd_equiv_of_right_inverse

added theorem continuous_linear_equiv.symm_equiv_of_inverse

added def continuous_linear_equiv.units_equiv_aut

added theorem continuous_linear_equiv.units_equiv_aut_apply

added theorem continuous_linear_equiv.units_equiv_aut_apply_symm

added theorem continuous_linear_equiv.units_equiv_aut_symm_apply

added theorem continuous_linear_map.apply_ker

added def continuous_linear_map.cod_restrict

added theorem continuous_linear_map.coe_cod_restrict

added theorem continuous_linear_map.coe_cod_restrict_apply

added theorem continuous_linear_map.coe_coprod

added theorem continuous_linear_map.coe_prod_map'

added theorem continuous_linear_map.coe_proj_ker_of_right_inverse_apply

added theorem continuous_linear_map.coe_subtype_val

added def continuous_linear_map.coprod

added theorem continuous_linear_map.coprod_apply

added theorem continuous_linear_map.is_closed_ker

added def continuous_linear_map.ker

added theorem continuous_linear_map.ker_coe

added theorem continuous_linear_map.mem_ker

added theorem continuous_linear_map.mem_range

deleted theorem continuous_linear_map.prod_map_apply

added def continuous_linear_map.proj_ker_of_right_inverse

added theorem continuous_linear_map.proj_ker_of_right_inverse_apply_idem

added theorem continuous_linear_map.proj_ker_of_right_inverse_comp_inv

added def continuous_linear_map.range

added theorem continuous_linear_map.range_coe

added theorem continuous_linear_map.smul_right_comp

added def continuous_linear_map.subtype_val

added theorem continuous_linear_map.subtype_val_apply