Commit 2023-02-28 18:01 be51120d

View on Github →

feat: port LinearAlgebra.Basis (#2435)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Equiv.lean

added def LinearEquiv.Simps.apply

Created Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.apply_eq_iff

added theorem Basis.basis_singleton_iff

added theorem Basis.coe_extend

added theorem Basis.coe_finTwoProd_repr

added theorem Basis.coe_mapCoeffs

added theorem Basis.coe_mk

added theorem Basis.coe_mkFinCons

added theorem Basis.coe_mkFinConsOfLe

added theorem Basis.coe_ofEquivFun

added theorem Basis.coe_ofVectorSpace

added theorem Basis.coe_of_repr

added theorem Basis.coe_reindex

added theorem Basis.coe_repr_symm

added theorem Basis.coe_sumCoords

added theorem Basis.coe_sumCoords_eq_finsum

added theorem Basis.coe_sumCoords_of_fintype

added def Basis.constr

added theorem Basis.constr_apply

added theorem Basis.constr_apply_fintype

added theorem Basis.constr_basis

added theorem Basis.constr_comp

added theorem Basis.constr_def

added theorem Basis.constr_eq

added theorem Basis.constr_range

added theorem Basis.constr_self

added def Basis.coord

added theorem Basis.coord_equivFun_symm

added theorem Basis.coord_repr_symm

added theorem Basis.coord_unitsSmul

added theorem Basis.dvd_coord_smul

added theorem Basis.eq_bot_of_rank_eq_zero

added theorem Basis.eq_of_apply_eq

added theorem Basis.eq_of_repr_eq_repr

added def Basis.equiv'

added theorem Basis.equiv'_apply

added theorem Basis.equiv'_symm_apply

added def Basis.equivFun

added theorem Basis.equivFun_apply

added theorem Basis.equivFun_self

added theorem Basis.equivFun_symm_apply

added theorem Basis.equiv_apply

added theorem Basis.equiv_refl

added theorem Basis.equiv_symm

added theorem Basis.equiv_trans

added theorem Basis.exists_basis

added theorem Basis.ext'

added theorem Basis.ext

added theorem Basis.ext_elem_iff

added theorem Basis.extend_apply_self

added theorem Basis.finTwoProd_one

added theorem Basis.finTwoProd_zero

added theorem Basis.forall_coord_eq_zero_iff

added def Basis.groupSmul

added theorem Basis.groupSmul_apply

added theorem Basis.groupSmul_span_eq_top

added theorem Basis.index_nonempty

added def Basis.isUnitSmul

added theorem Basis.isUnitSmul_apply

added def Basis.mapCoeffs

added theorem Basis.mapCoeffs_apply

added theorem Basis.map_apply

added theorem Basis.map_equiv

added theorem Basis.map_equivFun

added theorem Basis.maximal

added theorem Basis.mem_span_repr_support

added theorem Basis.mem_submodule_iff'

added theorem Basis.mem_submodule_iff

added theorem Basis.mk_apply

added theorem Basis.mk_coord_apply

added theorem Basis.mk_coord_apply_eq

added theorem Basis.mk_coord_apply_ne

added theorem Basis.mk_repr

added def Basis.ofEquivFun

added theorem Basis.ofEquivFun_equivFun

added theorem Basis.ofEquivFun_repr_apply

added theorem Basis.ofVectorSpaceIndex.linearIndependent

added theorem Basis.ofVectorSpace_apply_self

added theorem Basis.prod_apply

added theorem Basis.prod_apply_inl_fst

added theorem Basis.prod_apply_inl_snd

added theorem Basis.prod_apply_inr_fst

added theorem Basis.prod_apply_inr_snd

added theorem Basis.prod_repr_inl

added theorem Basis.prod_repr_inr

added theorem Basis.range_extend

added theorem Basis.range_ofVectorSpace

added theorem Basis.range_reindex

added def Basis.reindex

added def Basis.reindexFinsetRange

added theorem Basis.reindexFinsetRange_apply

added theorem Basis.reindexFinsetRange_repr

added theorem Basis.reindexFinsetRange_repr_self

added theorem Basis.reindexFinsetRange_self

added def Basis.reindexRange

added theorem Basis.reindexRange_apply

added theorem Basis.reindexRange_repr'

added theorem Basis.reindexRange_repr

added theorem Basis.reindexRange_repr_self

added theorem Basis.reindexRange_self

added theorem Basis.reindex_apply

added theorem Basis.reindex_refl

added theorem Basis.repr_apply_eq

added theorem Basis.repr_eq_iff'

added theorem Basis.repr_eq_iff

added theorem Basis.repr_injective

added theorem Basis.repr_range

added theorem Basis.repr_reindex

added theorem Basis.repr_reindex_apply

added theorem Basis.repr_self

added theorem Basis.repr_self_apply

added theorem Basis.repr_sum_self

added theorem Basis.repr_support_subset_of_mem_span

added theorem Basis.repr_symm_apply

added theorem Basis.repr_symm_single

added theorem Basis.repr_symm_single_one

added theorem Basis.repr_total

added theorem Basis.repr_unitsSmul

added theorem Basis.singleton_apply

added theorem Basis.singleton_repr

added theorem Basis.subset_extend

added theorem Basis.sumCoords_reindex

added theorem Basis.sumCoords_self_apply

added def Basis.sumExtendIndex

added theorem Basis.sum_equivFun

added theorem Basis.sum_repr

added theorem Basis.sum_repr_mul_repr

added theorem Basis.total_repr

added def Basis.unitsSmul

added theorem Basis.unitsSmul_apply

added theorem Basis.units_smul_span_eq_top

added structure Basis

added theorem LinearMap.exists_extend

added theorem LinearMap.exists_leftInverse_of_injective

added theorem LinearMap.exists_rightInverse_of_surjective

added theorem Module.card_fintype

added def Module.fintypeOfFintype

added theorem Submodule.exists_isCompl

added theorem Submodule.exists_le_ker_of_lt_top

added def Submodule.inductionOnRankAux

added theorem VectorSpace.card_fintype

added theorem atom_iff_nonzero_span

added theorem nonzero_span_atom

added theorem quotient_prod_linearEquiv

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

deleted theorem Submodule.Quotient.equiv_apply