Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-20 06:18 cbe80ed2

View on Github →

feat(linear_algebra/projection): projection to a subspace (#2739) Define equivalence between complement subspaces and projections.

Estimated changes

Modified src/algebra/module.lean

modified theorem submodule.add_mem_iff_left

modified theorem submodule.add_mem_iff_right

Modified src/data/prod.lean

added theorem prod.fst_eq_iff

added theorem prod.snd_eq_iff

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.coe_of_eq_apply

added theorem linear_equiv.coe_of_top_symm_apply

added def linear_equiv.of_eq

added theorem linear_equiv.of_eq_symm

modified theorem linear_equiv.of_top_symm_apply

added theorem linear_map.coe_quotient_inf_to_sup_quotient

added theorem linear_map.map_eq_top_iff

added theorem linear_map.map_le_map_iff'

modified theorem linear_map.map_le_map_iff

added theorem linear_map.quot_ker_equiv_range_apply_mk

added theorem linear_map.quot_ker_equiv_range_symm_apply_image

added theorem linear_map.quotient_inf_equiv_sup_quotient_apply_mk

added theorem linear_map.quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff

added theorem linear_map.quotient_inf_equiv_sup_quotient_symm_apply_left

added theorem linear_map.quotient_inf_equiv_sup_quotient_symm_apply_right

added theorem linear_map.range_range_restrict

added theorem submodule.coe_quot_equiv_of_eq_bot_symm

added theorem submodule.map_mkq_eq_top

added theorem submodule.mem_left_iff_eq_zero_of_disjoint

added theorem submodule.mem_right_iff_eq_zero_of_disjoint

added def submodule.quot_equiv_of_eq_bot

added theorem submodule.quot_equiv_of_eq_bot_apply_mk

added theorem submodule.quot_equiv_of_eq_bot_symm_apply

deleted theorem submodule.range_range_restrict

Modified src/linear_algebra/basis.lean

added theorem submodule.exists_is_compl

Modified src/linear_algebra/dimension.lean

Created src/linear_algebra/projection.lean

added theorem linear_map.is_compl_of_proj

added theorem linear_map.linear_proj_of_is_compl_of_proj

added theorem submodule.coe_is_compl_equiv_proj_apply

added theorem submodule.coe_is_compl_equiv_proj_symm_apply

added theorem submodule.coe_prod_equiv_of_is_compl'

added theorem submodule.coe_prod_equiv_of_is_compl

added def submodule.is_compl_equiv_proj

added def submodule.linear_proj_of_is_compl

added theorem submodule.linear_proj_of_is_compl_apply_eq_zero_iff

added theorem submodule.linear_proj_of_is_compl_apply_left

added theorem submodule.linear_proj_of_is_compl_apply_right'

added theorem submodule.linear_proj_of_is_compl_apply_right

added theorem submodule.linear_proj_of_is_compl_idempotent

added theorem submodule.linear_proj_of_is_compl_ker

added theorem submodule.linear_proj_of_is_compl_range

added theorem submodule.mk_quotient_equiv_of_is_compl_apply

added def submodule.prod_equiv_of_is_compl

added theorem submodule.prod_equiv_of_is_compl_symm_apply_fst_eq_zero

added theorem submodule.prod_equiv_of_is_compl_symm_apply_left

added theorem submodule.prod_equiv_of_is_compl_symm_apply_right

added theorem submodule.prod_equiv_of_is_compl_symm_apply_snd_eq_zero

added def submodule.quotient_equiv_of_is_compl

added theorem submodule.quotient_equiv_of_is_compl_apply_mk_coe

added theorem submodule.quotient_equiv_of_is_compl_symm_apply