Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-05 08:58 def4814c

View on Github →

refactor(topology/algebra/module): continuous semilinear maps (#9539) Generalize the theory of continuous linear maps to the semilinear setting. We introduce a notation ∘L for composition of continuous linear (i.e., not semilinear) maps, used sporadically to help with unification. See #8857 for a discussion of a related problem and fix.

Estimated changes

Modified src/analysis/complex/conformal.lean

Modified src/analysis/normed_space/complemented.lean

Modified src/topology/algebra/module.lean

modified theorem continuous_linear_equiv.apply_symm_apply

modified theorem continuous_linear_equiv.bijective

modified theorem continuous_linear_equiv.coe_apply

modified theorem continuous_linear_equiv.coe_coe

modified theorem continuous_linear_equiv.coe_comp_coe_symm

modified theorem continuous_linear_equiv.coe_def_rev

modified theorem continuous_linear_equiv.coe_inj

modified theorem continuous_linear_equiv.coe_injective

modified theorem continuous_linear_equiv.coe_prod

modified theorem continuous_linear_equiv.coe_symm_comp_coe

modified theorem continuous_linear_equiv.coe_to_homeomorph

modified theorem continuous_linear_equiv.coe_to_linear_equiv

modified theorem continuous_linear_equiv.comp_coe

modified theorem continuous_linear_equiv.eq_symm_apply

modified def continuous_linear_equiv.equiv_of_inverse

modified theorem continuous_linear_equiv.equiv_of_inverse_apply

modified theorem continuous_linear_equiv.ext

modified theorem continuous_linear_equiv.ext₁

modified theorem continuous_linear_equiv.image_closure

modified theorem continuous_linear_equiv.image_symm_image

modified theorem continuous_linear_equiv.injective

modified theorem continuous_linear_equiv.is_closed_image

modified theorem continuous_linear_equiv.map_add

modified theorem continuous_linear_equiv.map_eq_zero_iff

modified theorem continuous_linear_equiv.map_neg

modified theorem continuous_linear_equiv.map_nhds_eq

modified theorem continuous_linear_equiv.map_smul

added theorem continuous_linear_equiv.map_smulₛₗ

modified theorem continuous_linear_equiv.map_sub

modified theorem continuous_linear_equiv.map_zero

modified theorem continuous_linear_equiv.preimage_closure

modified def continuous_linear_equiv.prod

modified theorem continuous_linear_equiv.prod_apply

modified theorem continuous_linear_equiv.self_comp_symm

modified theorem continuous_linear_equiv.surjective

modified theorem continuous_linear_equiv.symm_apply_apply

modified theorem continuous_linear_equiv.symm_apply_eq

modified theorem continuous_linear_equiv.symm_comp_self

modified theorem continuous_linear_equiv.symm_equiv_of_inverse

modified theorem continuous_linear_equiv.symm_image_image

modified theorem continuous_linear_equiv.symm_map_nhds_eq

modified theorem continuous_linear_equiv.symm_symm

modified theorem continuous_linear_equiv.symm_symm_apply

modified theorem continuous_linear_equiv.symm_to_homeomorph

modified theorem continuous_linear_equiv.symm_to_linear_equiv

modified theorem continuous_linear_equiv.symm_trans_apply

modified def continuous_linear_equiv.to_continuous_linear_map

modified def continuous_linear_equiv.to_homeomorph

modified theorem continuous_linear_equiv.to_linear_equiv_injective

modified theorem continuous_linear_equiv.trans_apply

modified theorem continuous_linear_equiv.trans_to_linear_equiv

modified def continuous_linear_map.cod_restrict

modified theorem continuous_linear_map.coe_add'

modified theorem continuous_linear_map.coe_add

modified theorem continuous_linear_map.coe_cod_restrict

modified theorem continuous_linear_map.coe_cod_restrict_apply

modified theorem continuous_linear_map.coe_coe

modified theorem continuous_linear_map.coe_comp'

modified theorem continuous_linear_map.coe_comp

modified theorem continuous_linear_map.coe_coprod

modified theorem continuous_linear_map.coe_eq_id

modified theorem continuous_linear_map.coe_fn_injective

modified theorem continuous_linear_map.coe_fst'

modified theorem continuous_linear_map.coe_fst

modified theorem continuous_linear_map.coe_id'

modified theorem continuous_linear_map.coe_id

modified theorem continuous_linear_map.coe_inj

modified theorem continuous_linear_map.coe_injective

modified theorem continuous_linear_map.coe_inl

modified theorem continuous_linear_map.coe_inr

modified theorem continuous_linear_map.coe_mk'

modified theorem continuous_linear_map.coe_mk

modified theorem continuous_linear_map.coe_mul

modified theorem continuous_linear_map.coe_neg'

modified theorem continuous_linear_map.coe_neg

modified theorem continuous_linear_map.coe_prod

modified theorem continuous_linear_map.coe_prod_map'

modified theorem continuous_linear_map.coe_prod_map

modified theorem continuous_linear_map.coe_snd'

modified theorem continuous_linear_map.coe_snd

modified theorem continuous_linear_map.coe_sub'

modified theorem continuous_linear_map.coe_sub

modified theorem continuous_linear_map.coe_subtype_val

modified theorem continuous_linear_map.coe_sum'

modified theorem continuous_linear_map.coe_sum

modified theorem continuous_linear_map.coe_zero'

modified theorem continuous_linear_map.coe_zero

modified def continuous_linear_map.comp

modified theorem continuous_linear_map.comp_apply

modified theorem continuous_linear_map.comp_assoc

modified theorem continuous_linear_map.comp_id

modified theorem continuous_linear_map.comp_zero

modified def continuous_linear_map.coprod

modified theorem continuous_linear_map.coprod_apply

modified theorem continuous_linear_map.default_def

modified theorem continuous_linear_map.eq_on_closure_span

modified theorem continuous_linear_map.ext

modified theorem continuous_linear_map.ext_iff

modified theorem continuous_linear_map.ext_on

modified theorem continuous_linear_map.ext_ring

modified theorem continuous_linear_map.ext_ring_iff

modified def continuous_linear_map.fst

modified theorem continuous_linear_map.fst_comp_prod

modified theorem continuous_linear_map.fst_prod_snd

modified def continuous_linear_map.id

modified theorem continuous_linear_map.id_apply

modified theorem continuous_linear_map.id_comp

modified def continuous_linear_map.inl

modified theorem continuous_linear_map.inl_apply

modified def continuous_linear_map.inr

modified theorem continuous_linear_map.inr_apply

modified theorem continuous_linear_map.is_closed_ker

modified def continuous_linear_map.ker

modified theorem continuous_linear_map.ker_cod_restrict

modified theorem continuous_linear_map.ker_coe

modified theorem continuous_linear_map.ker_prod

modified theorem continuous_linear_map.map_smul

modified theorem continuous_linear_map.map_smul_of_tower

added theorem continuous_linear_map.map_smulₛₗ

modified theorem continuous_linear_map.map_sum

modified theorem continuous_linear_map.map_zero

modified theorem continuous_linear_map.mem_ker

modified theorem continuous_linear_map.mem_range

modified theorem continuous_linear_map.mem_range_self

modified theorem continuous_linear_map.mul_apply

modified theorem continuous_linear_map.mul_def

modified theorem continuous_linear_map.one_apply

modified theorem continuous_linear_map.one_def

modified theorem continuous_linear_map.prod_apply

modified def continuous_linear_map.prod_map

modified def continuous_linear_map.proj_ker_of_right_inverse

modified def continuous_linear_map.range

modified theorem continuous_linear_map.range_coe

modified theorem continuous_linear_map.range_coprod

modified theorem continuous_linear_map.range_prod_eq

modified theorem continuous_linear_map.range_prod_le

modified def continuous_linear_map.smul_right

modified theorem continuous_linear_map.smul_right_apply

modified theorem continuous_linear_map.smul_right_comp

modified theorem continuous_linear_map.smul_right_one_one

modified def continuous_linear_map.snd

modified theorem continuous_linear_map.snd_comp_prod

modified theorem continuous_linear_map.sub_apply'

modified def continuous_linear_map.subtype_val

modified theorem continuous_linear_map.subtype_val_apply

modified theorem continuous_linear_map.sum_apply

modified theorem continuous_linear_map.to_linear_map_eq_coe

modified theorem continuous_linear_map.zero_apply

modified theorem continuous_linear_map.zero_comp

modified theorem dense_range.topological_closure_map_submodule

modified theorem submodule.topological_closure_map