Commit 2023-02-14 14:29 336884cd

View on Github →

feat: port LinearAlgebra.Span (#2248)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Units.lean

Created Mathlib/LinearAlgebra/Span.lean

added theorem LinearEquiv.coord_self

added def LinearEquiv.toSpanNonzeroSingleton

added theorem LinearEquiv.toSpanNonzeroSingleton_one

added theorem LinearMap.eqOn_span'

added theorem LinearMap.eqOn_span

added theorem LinearMap.ext_on

added theorem LinearMap.ext_on_range

added theorem LinearMap.ker_toSpanSingleton

added theorem LinearMap.map_eq_top_iff

added theorem LinearMap.map_injective

added theorem LinearMap.map_le_map_iff'

added theorem LinearMap.span_singleton_eq_range

added theorem LinearMap.span_singleton_sup_ker_eq_top

added def LinearMap.toSpanSingleton

added theorem LinearMap.toSpanSingleton_one

added theorem LinearMap.toSpanSingleton_zero

added theorem Submodule.apply_mem_span_image_of_mem_span

added theorem Submodule.closure_le_toAddSubmonoid_span

added theorem Submodule.closure_subset_span

added theorem Submodule.coe_scott_continuous

added theorem Submodule.coe_sup

added theorem Submodule.coe_supᵢ_of_chain

added theorem Submodule.coe_supᵢ_of_directed

added theorem Submodule.comap_map_eq

added theorem Submodule.comap_map_eq_self

added theorem Submodule.disjoint_span_singleton'

added theorem Submodule.disjoint_span_singleton

added theorem Submodule.finite_span_isCompactElement

added theorem Submodule.finset_span_isCompactElement

added theorem Submodule.le_span_singleton_iff

added theorem Submodule.lt_sup_iff_not_mem

added theorem Submodule.map_span

added theorem Submodule.map_span_le

added theorem Submodule.map_subtype_span_singleton

added theorem Submodule.mem_prod

added theorem Submodule.mem_span

added theorem Submodule.mem_span_finite_of_mem_span

added theorem Submodule.mem_span_insert'

added theorem Submodule.mem_span_insert

added theorem Submodule.mem_span_pair

added theorem Submodule.mem_span_singleton

added theorem Submodule.mem_span_singleton_self

added theorem Submodule.mem_span_singleton_trans

added theorem Submodule.mem_sup'

added theorem Submodule.mem_sup

added theorem Submodule.mem_supᵢ

added theorem Submodule.mem_supᵢ_of_chain

added theorem Submodule.mem_supᵢ_of_directed

added theorem Submodule.mem_supₛ_of_directed

added theorem Submodule.nontrivial_span_singleton

added theorem Submodule.not_mem_span_of_apply_not_mem_span_image

added def Submodule.prod

added theorem Submodule.prod_bot

added theorem Submodule.prod_coe

added theorem Submodule.prod_inf_prod

added theorem Submodule.prod_sup_prod

added theorem Submodule.prod_top

added theorem Submodule.singleton_span_isCompactElement

added def Submodule.span

added theorem Submodule.span_attach_bunionᵢ

added theorem Submodule.span_closure

added theorem Submodule.span_coe_eq_restrictScalars

added theorem Submodule.span_empty

added theorem Submodule.span_eq

added theorem Submodule.span_eq_bot

added theorem Submodule.span_eq_of_le

added theorem Submodule.span_eq_span

added theorem Submodule.span_eq_supᵢ_of_singleton_spans

added theorem Submodule.span_image

added theorem Submodule.span_induction'

added theorem Submodule.span_induction

added theorem Submodule.span_insert

added theorem Submodule.span_insert_eq_span

added theorem Submodule.span_insert_zero

added theorem Submodule.span_int_eq

added theorem Submodule.span_int_eq_addSubgroup_closure

added theorem Submodule.span_le

added theorem Submodule.span_le_restrictScalars

added theorem Submodule.span_mono

added theorem Submodule.span_monotone

added theorem Submodule.span_nat_eq

added theorem Submodule.span_nat_eq_addSubmonoid_closure

added theorem Submodule.span_neg

added theorem Submodule.span_preimage_le

added theorem Submodule.span_prod_le

added theorem Submodule.span_range_eq_supᵢ

added theorem Submodule.span_singleton_eq_bot

added theorem Submodule.span_singleton_eq_range

added theorem Submodule.span_singleton_eq_span_singleton

added theorem Submodule.span_singleton_eq_top_iff

added theorem Submodule.span_singleton_group_smul_eq

added theorem Submodule.span_singleton_le_iff_mem

added theorem Submodule.span_singleton_smul_eq

added theorem Submodule.span_singleton_smul_le

added theorem Submodule.span_smul_eq_of_isUnit

added theorem Submodule.span_smul_le

added theorem Submodule.span_span

added theorem Submodule.span_span_coe_preimage

added theorem Submodule.span_span_of_tower

added theorem Submodule.span_subset_span

added theorem Submodule.span_sup

added theorem Submodule.span_union

added theorem Submodule.span_unionᵢ

added theorem Submodule.span_unionᵢ₂

added theorem Submodule.span_univ

added theorem Submodule.span_zero

added theorem Submodule.span_zero_singleton

added theorem Submodule.submodule_eq_supₛ_le_nonzero_spans

added theorem Submodule.subset_span

added theorem Submodule.subset_span_trans

added theorem Submodule.sup_span

added theorem Submodule.sup_toAddSubgroup

added theorem Submodule.sup_toAddSubmonoid

added theorem Submodule.supᵢ_eq_span

added theorem Submodule.supᵢ_induction'

added theorem Submodule.supᵢ_induction

added theorem Submodule.supᵢ_span

added theorem Submodule.supᵢ_toAddSubmonoid