Commit 2025-03-17 10:14 22d7a1ce

View on Github →

chore(LinearAlgebra/Basis): redo the file structure of Defs, Basic (#22066) This PR reorganizes the files LinearAlgebra.Basis.Defs and LinearAlgebra.Basis.Basic: sorting the declarations, splitting off ones that need more imports, and generally cleaning up the structure. After this PR, the basic files for Basis are:

  • Basis.Defs: definition of a basis; extensionality of and w.r.t. bases; operations such as repr, equivFun, reindex, map, constr, coord.
  • Basis.Basic: equivalence between two definitions of basis (as linear independent spanning family, or as equivalence to finsupp); assorted small lemmas.
  • Basis.Fin: bases indexed by Fin (extend a basis using Fin.cons, ...)
  • Basis.Prod: basis for the product of modules
  • Basis.SMul: scalar multiplication of basis vectors
  • Basis.Submodule: bases for submodules (membership tests, restricting bases to submodules, using bases for induction, ...)

Estimated changes

deleted theorem Basis.coe_finTwoProd_repr
deleted theorem Basis.coe_mkFinCons
deleted theorem Basis.coe_mkFinConsOfLE
deleted theorem Basis.coord_unitsSMul
deleted theorem Basis.finTwoProd_one
deleted theorem Basis.finTwoProd_zero
deleted def Basis.groupSMul
deleted theorem Basis.groupSMul_apply
added theorem Basis.index_nonempty
deleted def Basis.isUnitSMul
deleted theorem Basis.isUnitSMul_apply
deleted theorem Basis.mem_center_iff
added theorem Basis.mem_span_image
deleted theorem Basis.prod_apply
deleted theorem Basis.prod_apply_inl_fst
deleted theorem Basis.prod_apply_inl_snd
deleted theorem Basis.prod_apply_inr_fst
deleted theorem Basis.prod_apply_inr_snd
deleted theorem Basis.prod_repr_inl
deleted theorem Basis.prod_repr_inr
deleted theorem Basis.repr_isUnitSMul
added theorem Basis.repr_range
deleted theorem Basis.repr_unitsSMul
added theorem Basis.singleton_apply
added theorem Basis.singleton_repr
deleted def Basis.unitsSMul
deleted theorem Basis.unitsSMul_apply
deleted theorem Basis.coe_smul
modified theorem Basis.constr_apply_fintype
modified theorem Basis.coord_equivFun_symm
deleted theorem Basis.index_nonempty
deleted theorem Basis.mem_span_image
deleted theorem Basis.mem_submodule_iff'
deleted theorem Basis.mem_submodule_iff
modified theorem Basis.reindex_refl
deleted theorem Basis.repr_range
deleted theorem Basis.repr_smul
deleted theorem Basis.self_mem_span_image
deleted theorem Basis.singleton_apply
deleted theorem Basis.singleton_repr
deleted theorem Basis.smul_apply
deleted theorem Basis.smul_eq_map
added theorem Basis.coe_mkFinCons
added theorem Basis.finTwoProd_one
added theorem Basis.finTwoProd_zero
added theorem Basis.prod_apply
added theorem Basis.prod_repr_inl
added theorem Basis.prod_repr_inr
added theorem Basis.coe_smul
added theorem Basis.coord_unitsSMul
added def Basis.groupSMul
added theorem Basis.groupSMul_apply
added def Basis.isUnitSMul
added theorem Basis.isUnitSMul_apply
added theorem Basis.repr_isUnitSMul
added theorem Basis.repr_smul
added theorem Basis.repr_unitsSMul
added theorem Basis.smul_apply
added theorem Basis.smul_eq_map
added def Basis.unitsSMul
added theorem Basis.unitsSMul_apply
added theorem Basis.mem_center_iff