Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-05 09:21 10a586b1

View on Github →

feat(linear_algebra): add module (vector_space) structure for function spaces

Estimated changes

Modified src/linear_algebra/basic.lean

added def equiv.to_linear_equiv

added theorem linear_equiv.eq_bot_of_equiv

added def linear_equiv.smul_of_ne_zero

added def linear_equiv.smul_of_unit

added theorem linear_map.comp_cod_restrict

added def linear_map.diag

added theorem linear_map.disjoint_std_basis_std_basis

added theorem linear_map.infi_ker_proj

added def linear_map.infi_ker_proj_equiv

added theorem linear_map.infi_ker_proj_le_supr_range_std_basis

added theorem linear_map.ker_pi

added theorem linear_map.ker_std_basis

added def linear_map.pi

added theorem linear_map.pi_apply

added theorem linear_map.pi_comp

added theorem linear_map.pi_eq_zero

added theorem linear_map.pi_zero

added def linear_map.proj

added theorem linear_map.proj_apply

added theorem linear_map.proj_comp_std_basis

added theorem linear_map.proj_pi

added theorem linear_map.proj_std_basis_ne

added theorem linear_map.proj_std_basis_same

added def linear_map.std_basis

added theorem linear_map.std_basis_apply

added theorem linear_map.std_basis_ne

added theorem linear_map.std_basis_same

added theorem linear_map.subtype_comp_cod_restrict

added theorem linear_map.supr_range_std_basis

added theorem linear_map.supr_range_std_basis_eq_infi_ker_proj

added theorem linear_map.supr_range_std_basis_le_infi_ker_proj

added theorem linear_map.update_apply

added theorem submodule.disjoint_iff_comap_eq_bot

added theorem submodule.eq_zero_of_bot_submodule

added theorem submodule.mem_supr_of_mem

added theorem submodule.span_univ

Modified src/linear_algebra/basis.lean

added theorem linear_independent_Union_finite

added theorem pi.is_basis_fun

added theorem pi.is_basis_std_basis

added theorem pi.linear_independent_std_basis

Modified src/linear_algebra/dimension.lean

added theorem dim_fun'

added theorem dim_fun

added theorem dim_pi