Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-27 09:35 3397560e

View on Github →

chore(topology/algebra/module/basic): remove continuous_linear_map.ker and continuous_linear_map.range (#16208) This PR removes continuous_linear_map.ker and continuous_linear_map.range, which are now obsolete since linear_map.ker and linear_map.range are defined for any linear_map_class morphism.

Estimated changes

Modified src/analysis/calculus/implicit.lean

modified theorem has_strict_fderiv_at.eq_implicit_function

modified def has_strict_fderiv_at.implicit_function

modified def has_strict_fderiv_at.implicit_to_local_homeomorph

modified theorem has_strict_fderiv_at.map_implicit_function_eq

modified theorem has_strict_fderiv_at.to_implicit_function

Modified src/analysis/calculus/inverse.lean

Modified src/analysis/calculus/lagrange_multipliers.lean

Modified src/analysis/inner_product_space/basic.lean

modified theorem orthogonal_eq_inter

Modified src/analysis/inner_product_space/dual.lean

Modified src/analysis/inner_product_space/lax_milgram.lean

modified theorem is_coercive.closed_range

modified theorem is_coercive.ker_eq_bot

modified theorem is_coercive.range_eq_top

Modified src/analysis/inner_product_space/projection.lean

Modified src/analysis/normed_space/banach.lean

modified theorem continuous_linear_equiv.coe_fn_of_bijective

modified theorem continuous_linear_equiv.coe_of_bijective

modified theorem continuous_linear_equiv.of_bijective_apply_symm_apply

modified theorem continuous_linear_equiv.of_bijective_symm_apply_apply

modified theorem continuous_linear_map.exists_nonlinear_right_inverse_of_surjective

modified theorem continuous_linear_map.nonlinear_right_inverse_of_surjective_nnnorm_pos

Modified src/analysis/normed_space/complemented.lean

modified def continuous_linear_map.equiv_prod_of_surjective_of_is_compl

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/geometry/manifold/mfderiv.lean

Modified src/geometry/manifold/whitney_embedding.lean

Modified src/linear_algebra/basic.lean

modified theorem linear_map.ker_eq_bot

modified theorem linear_map.sub_mem_ker_iff

added theorem linear_map_class.ker_eq_bot

Modified src/linear_algebra/prod.lean

Modified src/linear_algebra/projection.lean

Modified src/measure_theory/function/continuous_map_dense.lean

Modified src/measure_theory/function/lp_space.lean

Modified src/topology/algebra/module/basic.lean

deleted theorem continuous_linear_map.apply_ker

modified theorem continuous_linear_map.infi_ker_proj

modified theorem continuous_linear_map.is_closed_ker

deleted def continuous_linear_map.ker

deleted theorem continuous_linear_map.ker_coe

deleted theorem continuous_linear_map.mem_ker

deleted theorem continuous_linear_map.mem_range

deleted theorem continuous_linear_map.mem_range_self

deleted def continuous_linear_map.range

deleted theorem continuous_linear_map.range_coe

modified theorem continuous_linear_map.range_prod_eq

deleted theorem continuous_linear_map.range_prod_le

modified theorem submodule.ker_subtypeL

modified theorem submodule.range_subtypeL

Modified src/topology/algebra/module/finite_dimension.lean