Commit 2025-07-24 16:31 66baa859

View on Github →

chore: rename Basis to Module.Basis (#27381) Many other things can have bases.

Estimated changes

Modified Mathlib/Algebra/Azumaya/Matrix.lean

Modified Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Projective.lean

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

Modified Mathlib/Algebra/Group/UniqueProds/VectorSpace.lean

Modified Mathlib/Algebra/Lie/Rank.lean

Modified Mathlib/Algebra/Module/Lattice.lean

deleted theorem Basis.extendOfIsLattice_apply

added theorem Module.Basis.extendOfIsLattice_apply

Modified Mathlib/Algebra/Module/LinearMap/Polynomial.lean

Modified Mathlib/Algebra/Module/Presentation/Differentials.lean

Modified Mathlib/Algebra/Module/SpanRank.lean

added theorem Module.Basis.mk_eq_spanRank

deleted theorem Submodule.Basis.mk_eq_spanRank

modified theorem Submodule.rank_eq_spanRank_of_free

modified theorem Submodule.rank_le_spanRank

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

deleted def Basis.ofZLatticeBasis

deleted theorem Basis.ofZLatticeBasis_apply

deleted theorem Basis.ofZLatticeBasis_comap

deleted theorem Basis.ofZLatticeBasis_repr_apply

deleted theorem Basis.ofZLatticeBasis_span

deleted def Basis.ofZLatticeComap

deleted theorem Basis.ofZLatticeComap_apply

deleted theorem Basis.ofZLatticeComap_repr_apply

added def Module.Basis.ofZLatticeBasis

added theorem Module.Basis.ofZLatticeBasis_apply

added theorem Module.Basis.ofZLatticeBasis_comap

added theorem Module.Basis.ofZLatticeBasis_repr_apply

added theorem Module.Basis.ofZLatticeBasis_span

added def Module.Basis.ofZLatticeComap

added theorem Module.Basis.ofZLatticeComap_apply

added theorem Module.Basis.ofZLatticeComap_repr_apply

Modified Mathlib/Algebra/Polynomial/Basis.lean

Modified Mathlib/Algebra/Polynomial/Sequence.lean

Modified Mathlib/Algebra/Quaternion.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

modified def SkewMonoidAlgebra.basisSingleOne

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Analysis/BoxIntegral/UnitPartition.lean

Modified Mathlib/Analysis/Complex/Tietze.lean

Modified Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthonormal.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

deleted theorem Basis.coe_toOrthonormalBasis

deleted theorem Basis.coe_toOrthonormalBasis_repr

deleted theorem Basis.coe_toOrthonormalBasis_repr_symm

deleted theorem Basis.toBasis_toOrthonormalBasis

deleted def Basis.toOrthonormalBasis

added theorem Module.Basis.coe_toOrthonormalBasis

added theorem Module.Basis.coe_toOrthonormalBasis_repr

added theorem Module.Basis.coe_toOrthonormalBasis_repr_symm

added theorem Module.Basis.toBasis_toOrthonormalBasis

added def Module.Basis.toOrthonormalBasis

Modified Mathlib/Analysis/InnerProductSpace/ProdL2.lean

Modified Mathlib/Analysis/InnerProductSpace/Subspace.lean

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

deleted theorem Basis.exists_opNNNorm_le

deleted theorem Basis.exists_opNorm_le

deleted theorem Basis.opNNNorm_le

deleted theorem Basis.opNorm_le

added theorem Module.Basis.exists_opNNNorm_le

added theorem Module.Basis.exists_opNorm_le

added theorem Module.Basis.opNNNorm_le

added theorem Module.Basis.opNorm_le

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

deleted theorem Basis.ext_linearIsometry

deleted theorem Basis.ext_linearIsometryEquiv

added theorem Module.Basis.ext_linearIsometry

added theorem Module.Basis.ext_linearIsometryEquiv

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

deleted def Basis.norm

deleted theorem Basis.norm_extends

deleted theorem Basis.norm_isNonarchimedean

deleted theorem Basis.norm_mul_le_const_mul_norm

deleted theorem Basis.norm_repr_le_norm

deleted theorem Basis.norm_smul

added def Module.Basis.norm

added theorem Module.Basis.norm_extends

added theorem Module.Basis.norm_isNonarchimedean

added theorem Module.Basis.norm_mul_le_const_mul_norm

added theorem Module.Basis.norm_repr_le_norm

added theorem Module.Basis.norm_smul

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean

deleted def Basis.mapPowExpCharPowOfIsSeparable

added def Module.Basis.mapPowExpCharPowOfIsSeparable

Modified Mathlib/FieldTheory/PurelyInseparable/Tower.lean

Modified Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

deleted theorem Basis.ext_alternating

added theorem Module.Basis.ext_alternating

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

deleted theorem Basis.basis_singleton_iff

deleted theorem Basis.coe_mk

deleted theorem Basis.index_nonempty

deleted theorem Basis.maximal

deleted theorem Basis.mem_span_image

deleted theorem Basis.mem_span_repr_support

deleted theorem Basis.mk_apply

deleted theorem Basis.mk_coord_apply

deleted theorem Basis.mk_coord_apply_eq

deleted theorem Basis.mk_coord_apply_ne

deleted theorem Basis.mk_repr

deleted theorem Basis.repr_range

deleted theorem Basis.repr_support_subset_of_mem_span

deleted theorem Basis.self_mem_span_image

deleted theorem Basis.singleton_apply

deleted theorem Basis.singleton_repr

added theorem Module.Basis.basis_singleton_iff

added theorem Module.Basis.coe_mk

added theorem Module.Basis.index_nonempty

added theorem Module.Basis.maximal

added theorem Module.Basis.mem_span_image

added theorem Module.Basis.mem_span_repr_support

added theorem Module.Basis.mk_apply

added theorem Module.Basis.mk_coord_apply

added theorem Module.Basis.mk_coord_apply_eq

added theorem Module.Basis.mk_coord_apply_ne

added theorem Module.Basis.mk_repr

added theorem Module.Basis.repr_range

added theorem Module.Basis.repr_support_subset_of_mem_span

added theorem Module.Basis.self_mem_span_image

added theorem Module.Basis.singleton_apply

added theorem Module.Basis.singleton_repr

Modified Mathlib/LinearAlgebra/Basis/Bilinear.lean

Modified Mathlib/LinearAlgebra/Basis/Cardinality.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

deleted theorem Basis.apply_eq_iff

deleted theorem Basis.coe_map

deleted theorem Basis.coe_mapCoeffs

deleted theorem Basis.coe_ofEquivFun

deleted theorem Basis.coe_ofRepr

deleted theorem Basis.coe_reindex

deleted theorem Basis.coe_repr_symm

deleted theorem Basis.coe_sumCoords

deleted theorem Basis.coe_sumCoords_eq_finsum

deleted theorem Basis.coe_sumCoords_of_fintype

deleted def Basis.constr

deleted theorem Basis.constr_apply

deleted theorem Basis.constr_apply_fintype

deleted theorem Basis.constr_basis

deleted theorem Basis.constr_comp

deleted theorem Basis.constr_def

deleted theorem Basis.constr_eq

deleted theorem Basis.constr_range

deleted theorem Basis.constr_self

deleted def Basis.coord

deleted theorem Basis.coord_equivFun_symm

deleted theorem Basis.coord_repr_symm

deleted theorem Basis.dvd_coord_smul

deleted theorem Basis.eq_ofRepr_eq_repr

deleted theorem Basis.eq_of_apply_eq

deleted def Basis.equiv'

deleted theorem Basis.equiv'_apply

deleted theorem Basis.equiv'_symm_apply

deleted def Basis.equivFun

deleted theorem Basis.equivFun_apply

deleted theorem Basis.equivFun_ofEquivFun

deleted theorem Basis.equivFun_self

deleted theorem Basis.equivFun_symm_apply

deleted theorem Basis.equiv_apply

deleted theorem Basis.equiv_refl

deleted theorem Basis.equiv_symm

deleted theorem Basis.equiv_trans

deleted theorem Basis.ext'

deleted theorem Basis.ext

deleted theorem Basis.ext_elem_iff

deleted theorem Basis.forall_coord_eq_zero_iff

deleted theorem Basis.linearCombination_repr

deleted def Basis.mapCoeffs

deleted theorem Basis.mapCoeffs_apply

deleted theorem Basis.map_apply

deleted theorem Basis.map_equiv

deleted theorem Basis.map_equivFun

deleted def Basis.ofEquivFun

deleted theorem Basis.ofEquivFun_equivFun

deleted theorem Basis.ofEquivFun_repr_apply

deleted theorem Basis.range_reindex

deleted def Basis.reindex

deleted def Basis.reindexFinsetRange

deleted theorem Basis.reindexFinsetRange_apply

deleted theorem Basis.reindexFinsetRange_repr

deleted theorem Basis.reindexFinsetRange_repr_self

deleted theorem Basis.reindexFinsetRange_self

deleted def Basis.reindexRange

deleted theorem Basis.reindexRange_apply

deleted theorem Basis.reindexRange_repr'

deleted theorem Basis.reindexRange_repr

deleted theorem Basis.reindexRange_repr_self

deleted theorem Basis.reindexRange_self

deleted theorem Basis.reindex_apply

deleted theorem Basis.reindex_refl

deleted theorem Basis.repr_apply_eq

deleted theorem Basis.repr_eq_iff'

deleted theorem Basis.repr_eq_iff

deleted theorem Basis.repr_injective

deleted theorem Basis.repr_linearCombination

deleted theorem Basis.repr_reindex

deleted theorem Basis.repr_reindex_apply

deleted theorem Basis.repr_self

deleted theorem Basis.repr_self_apply

deleted theorem Basis.repr_sum_self

deleted theorem Basis.repr_symm_apply

deleted theorem Basis.repr_symm_single

deleted theorem Basis.repr_symm_single_one

deleted theorem Basis.sumCoords_reindex

deleted theorem Basis.sumCoords_self_apply

deleted theorem Basis.sum_equivFun

deleted theorem Basis.sum_repr

deleted theorem Basis.sum_repr_mul_repr

deleted structure Basis

added theorem Module.Basis.apply_eq_iff

added theorem Module.Basis.coe_map

added theorem Module.Basis.coe_mapCoeffs

added theorem Module.Basis.coe_ofEquivFun

added theorem Module.Basis.coe_ofRepr

added theorem Module.Basis.coe_reindex

added theorem Module.Basis.coe_repr_symm

added theorem Module.Basis.coe_sumCoords

added theorem Module.Basis.coe_sumCoords_eq_finsum

added theorem Module.Basis.coe_sumCoords_of_fintype

added def Module.Basis.constr

added theorem Module.Basis.constr_apply

added theorem Module.Basis.constr_apply_fintype

added theorem Module.Basis.constr_basis

added theorem Module.Basis.constr_comp

added theorem Module.Basis.constr_def

added theorem Module.Basis.constr_eq

added theorem Module.Basis.constr_range

added theorem Module.Basis.constr_self

added def Module.Basis.coord

added theorem Module.Basis.coord_equivFun_symm

added theorem Module.Basis.coord_repr_symm

added theorem Module.Basis.dvd_coord_smul

added theorem Module.Basis.eq_ofRepr_eq_repr

added theorem Module.Basis.eq_of_apply_eq

added def Module.Basis.equiv'

added theorem Module.Basis.equiv'_apply

added theorem Module.Basis.equiv'_symm_apply

added def Module.Basis.equivFun

added theorem Module.Basis.equivFun_apply

added theorem Module.Basis.equivFun_ofEquivFun

added theorem Module.Basis.equivFun_self

added theorem Module.Basis.equivFun_symm_apply

added theorem Module.Basis.equiv_apply

added theorem Module.Basis.equiv_refl

added theorem Module.Basis.equiv_symm

added theorem Module.Basis.equiv_trans

added theorem Module.Basis.ext'

added theorem Module.Basis.ext

added theorem Module.Basis.ext_elem_iff

added theorem Module.Basis.forall_coord_eq_zero_iff

added theorem Module.Basis.linearCombination_repr

added def Module.Basis.mapCoeffs

added theorem Module.Basis.mapCoeffs_apply

added theorem Module.Basis.map_apply

added theorem Module.Basis.map_equiv

added theorem Module.Basis.map_equivFun

added def Module.Basis.ofEquivFun

added theorem Module.Basis.ofEquivFun_equivFun

added theorem Module.Basis.ofEquivFun_repr_apply

added theorem Module.Basis.range_reindex

added def Module.Basis.reindex

added def Module.Basis.reindexFinsetRange

added theorem Module.Basis.reindexFinsetRange_apply

added theorem Module.Basis.reindexFinsetRange_repr

added theorem Module.Basis.reindexFinsetRange_repr_self

added theorem Module.Basis.reindexFinsetRange_self

added def Module.Basis.reindexRange

added theorem Module.Basis.reindexRange_apply

added theorem Module.Basis.reindexRange_repr'

added theorem Module.Basis.reindexRange_repr

added theorem Module.Basis.reindexRange_repr_self

added theorem Module.Basis.reindexRange_self

added theorem Module.Basis.reindex_apply

added theorem Module.Basis.reindex_refl

added theorem Module.Basis.repr_apply_eq

added theorem Module.Basis.repr_eq_iff'

added theorem Module.Basis.repr_eq_iff

added theorem Module.Basis.repr_injective

added theorem Module.Basis.repr_linearCombination

added theorem Module.Basis.repr_reindex

added theorem Module.Basis.repr_reindex_apply

added theorem Module.Basis.repr_self

added theorem Module.Basis.repr_self_apply

added theorem Module.Basis.repr_sum_self

added theorem Module.Basis.repr_symm_apply

added theorem Module.Basis.repr_symm_single

added theorem Module.Basis.repr_symm_single_one

added theorem Module.Basis.sumCoords_reindex

added theorem Module.Basis.sumCoords_self_apply

added theorem Module.Basis.sum_equivFun

added theorem Module.Basis.sum_repr

added theorem Module.Basis.sum_repr_mul_repr

added structure Module.Basis

modified theorem Module.card_fintype

modified def Module.fintypeOfFintype

Modified Mathlib/LinearAlgebra/Basis/Exact.lean

Modified Mathlib/LinearAlgebra/Basis/Fin.lean

deleted theorem Basis.coe_finTwoProd_repr

deleted theorem Basis.coe_mkFinCons

deleted theorem Basis.coe_mkFinConsOfLE

deleted theorem Basis.finTwoProd_one

deleted theorem Basis.finTwoProd_zero

added theorem Module.Basis.coe_finTwoProd_repr

added theorem Module.Basis.coe_mkFinCons

added theorem Module.Basis.coe_mkFinConsOfLE

added theorem Module.Basis.finTwoProd_one

added theorem Module.Basis.finTwoProd_zero

Modified Mathlib/LinearAlgebra/Basis/Flag.lean

deleted def Basis.flag

deleted theorem Basis.flag_covBy

deleted theorem Basis.flag_last

deleted theorem Basis.flag_le_flag

deleted theorem Basis.flag_le_iff

deleted theorem Basis.flag_le_ker_coord

deleted theorem Basis.flag_le_ker_coord_iff

deleted theorem Basis.flag_le_ker_dual

deleted theorem Basis.flag_lt_flag

deleted theorem Basis.flag_mono

deleted theorem Basis.flag_strictMono

deleted theorem Basis.flag_succ

deleted theorem Basis.flag_wcovBy

deleted theorem Basis.flag_zero

deleted theorem Basis.isChain_range_flag

deleted theorem Basis.isMaxChain_range_flag

deleted theorem Basis.mem_toFlag

deleted theorem Basis.self_mem_flag

deleted theorem Basis.self_mem_flag_iff

deleted def Basis.toFlag

added def Module.Basis.flag

added theorem Module.Basis.flag_covBy

added theorem Module.Basis.flag_last

added theorem Module.Basis.flag_le_flag

added theorem Module.Basis.flag_le_iff

added theorem Module.Basis.flag_le_ker_coord

added theorem Module.Basis.flag_le_ker_coord_iff

added theorem Module.Basis.flag_le_ker_dual

added theorem Module.Basis.flag_lt_flag

added theorem Module.Basis.flag_mono

added theorem Module.Basis.flag_strictMono

added theorem Module.Basis.flag_succ

added theorem Module.Basis.flag_wcovBy

added theorem Module.Basis.flag_zero

added theorem Module.Basis.isChain_range_flag

added theorem Module.Basis.isMaxChain_range_flag

added theorem Module.Basis.mem_toFlag

added theorem Module.Basis.self_mem_flag

added theorem Module.Basis.self_mem_flag_iff

added def Module.Basis.toFlag

Modified Mathlib/LinearAlgebra/Basis/MulOpposite.lean

deleted theorem Basis.mulOpposite_apply

deleted theorem Basis.mulOpposite_repr_eq

deleted theorem Basis.mulOpposite_repr_op

deleted theorem Basis.repr_unop_eq_mulOpposite_repr

added theorem Module.Basis.mulOpposite_apply

added theorem Module.Basis.mulOpposite_repr_eq

added theorem Module.Basis.mulOpposite_repr_op

added theorem Module.Basis.repr_unop_eq_mulOpposite_repr

Modified Mathlib/LinearAlgebra/Basis/Prod.lean

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

added theorem Module.Basis.prod_apply

added theorem Module.Basis.prod_apply_inl_fst

added theorem Module.Basis.prod_apply_inl_snd

added theorem Module.Basis.prod_apply_inr_fst

added theorem Module.Basis.prod_apply_inr_snd

added theorem Module.Basis.prod_repr_inl

added theorem Module.Basis.prod_repr_inr

Modified Mathlib/LinearAlgebra/Basis/SMul.lean

deleted theorem Basis.coe_smul

deleted theorem Basis.coord_unitsSMul

deleted def Basis.groupSMul

deleted theorem Basis.groupSMul_apply

deleted theorem Basis.groupSMul_span_eq_top

deleted def Basis.isUnitSMul

deleted theorem Basis.isUnitSMul_apply

deleted theorem Basis.repr_isUnitSMul

deleted theorem Basis.repr_smul

deleted theorem Basis.repr_unitsSMul

deleted theorem Basis.smul_apply

deleted theorem Basis.smul_eq_map

deleted def Basis.unitsSMul

deleted theorem Basis.unitsSMul_apply

deleted theorem Basis.units_smul_span_eq_top

added theorem Module.Basis.coe_smul

added theorem Module.Basis.coord_unitsSMul

added def Module.Basis.groupSMul

added theorem Module.Basis.groupSMul_apply

added theorem Module.Basis.groupSMul_span_eq_top

added def Module.Basis.isUnitSMul

added theorem Module.Basis.isUnitSMul_apply

added theorem Module.Basis.repr_isUnitSMul

added theorem Module.Basis.repr_smul

added theorem Module.Basis.repr_unitsSMul

added theorem Module.Basis.smul_apply

added theorem Module.Basis.smul_eq_map

added def Module.Basis.unitsSMul

added theorem Module.Basis.unitsSMul_apply

added theorem Module.Basis.units_smul_span_eq_top

Modified Mathlib/LinearAlgebra/Basis/Submodule.lean

deleted theorem Basis.addSubgroupOfClosure_apply

deleted theorem Basis.addSubgroupOfClosure_repr_apply

deleted theorem Basis.eq_bot_of_rank_eq_zero

deleted theorem Basis.mem_center_iff

deleted theorem Basis.mem_span_iff_repr_mem

deleted theorem Basis.mem_submodule_iff'

deleted theorem Basis.mem_submodule_iff

deleted theorem Basis.restrictScalars_apply

deleted theorem Basis.restrictScalars_repr_apply

added theorem Module.Basis.Basis.eq_bot_of_rank_eq_zero

added theorem Module.Basis.Module.Basis.addSubgroupOfClosure_apply

added theorem Module.Basis.Module.Basis.addSubgroupOfClosure_repr_apply

added theorem Module.Basis.Module.Basis.mem_center_iff

added theorem Module.Basis.Module.Basis.mem_span_iff_repr_mem

added theorem Module.Basis.Module.Basis.restrictScalars_apply

added theorem Module.Basis.Module.Basis.restrictScalars_repr_apply

added def Module.Basis.Submodule.inductionOnRankAux

added theorem Module.Basis.mem_submodule_iff'

added theorem Module.Basis.mem_submodule_iff

deleted def Submodule.inductionOnRankAux

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

deleted theorem Basis.coe_extend

deleted theorem Basis.coe_extendLe

deleted theorem Basis.coe_ofSpan

deleted theorem Basis.coe_ofVectorSpace

deleted theorem Basis.exists_basis

deleted theorem Basis.extendLe_apply_self

deleted theorem Basis.extendLe_subset

deleted theorem Basis.extend_apply_self

deleted theorem Basis.ofSpan_apply_self

deleted theorem Basis.ofSpan_subset

deleted theorem Basis.ofVectorSpaceIndex.linearIndependent

deleted theorem Basis.ofVectorSpace_apply_self

deleted theorem Basis.range_extend

deleted theorem Basis.range_extendLe

deleted theorem Basis.range_ofSpan

deleted theorem Basis.range_ofVectorSpace

deleted theorem Basis.subset_extend

deleted theorem Basis.subset_extendLe

deleted def Basis.sumExtendIndex

added theorem Module.Basis.coe_extend

added theorem Module.Basis.coe_extendLe

added theorem Module.Basis.coe_ofSpan

added theorem Module.Basis.coe_ofVectorSpace

added theorem Module.Basis.exists_basis

added theorem Module.Basis.extendLe_apply_self

added theorem Module.Basis.extendLe_subset

added theorem Module.Basis.extend_apply_self

added theorem Module.Basis.ofSpan_apply_self

added theorem Module.Basis.ofSpan_subset

added theorem Module.Basis.ofVectorSpaceIndex.linearIndependent

added theorem Module.Basis.ofVectorSpace_apply_self

added theorem Module.Basis.range_extend

added theorem Module.Basis.range_extendLe

added theorem Module.Basis.range_ofSpan

added theorem Module.Basis.range_ofVectorSpace

added theorem Module.Basis.subset_extend

added theorem Module.Basis.subset_extendLe

added def Module.Basis.sumExtendIndex

Modified Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Hom.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/Charpoly/BaseChange.lean

Modified Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

deleted theorem Basis.det_apply

deleted theorem Basis.det_basis

deleted theorem Basis.det_comp

deleted theorem Basis.det_comp_basis

deleted theorem Basis.det_inv

deleted theorem Basis.det_isEmpty

deleted theorem Basis.det_isUnitSMul

deleted theorem Basis.det_map'

deleted theorem Basis.det_map

deleted theorem Basis.det_ne_zero

deleted theorem Basis.det_reindex'

deleted theorem Basis.det_reindex

deleted theorem Basis.det_reindex_symm

deleted theorem Basis.det_self

deleted theorem Basis.det_smul_mk_coord_eq_det_update

deleted theorem Basis.det_unitsSMul

deleted theorem Basis.det_unitsSMul_self

deleted theorem Basis.isUnit_det

deleted theorem Basis.smul_det

added theorem Module.Basis.det_apply

added theorem Module.Basis.det_basis

added theorem Module.Basis.det_comp

added theorem Module.Basis.det_comp_basis

added theorem Module.Basis.det_inv

added theorem Module.Basis.det_isEmpty

added theorem Module.Basis.det_isUnitSMul

added theorem Module.Basis.det_map'

added theorem Module.Basis.det_map

added theorem Module.Basis.det_ne_zero

added theorem Module.Basis.det_reindex'

added theorem Module.Basis.det_reindex

added theorem Module.Basis.det_reindex_symm

added theorem Module.Basis.det_self

added theorem Module.Basis.det_smul_mk_coord_eq_det_update

added theorem Module.Basis.det_unitsSMul

added theorem Module.Basis.det_unitsSMul_self

added theorem Module.Basis.isUnit_det

added theorem Module.Basis.is_basis_iff_det

added theorem Module.Basis.smul_det

deleted theorem is_basis_iff_det

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

deleted theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0

added theorem Module.Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

deleted theorem Basis.finite_index_of_rank_lt_aleph0

deleted theorem Basis.nonempty_fintype_index_of_rank_lt_aleph0

added theorem Module.Basis.finite_index_of_rank_lt_aleph0

added theorem Module.Basis.nonempty_fintype_index_of_rank_lt_aleph0

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

deleted theorem Basis.card_le_card_of_le

deleted theorem Basis.card_le_card_of_linearIndependent

deleted theorem Basis.card_le_card_of_submodule

deleted def Basis.indexEquiv

deleted theorem Basis.le_span

deleted theorem Basis.mk_eq_rank''

deleted theorem Basis.mk_eq_rank'.{m}

deleted theorem Basis.mk_eq_rank

deleted theorem Basis.mk_range_eq_rank

added theorem Module.Basis.card_le_card_of_le

added theorem Module.Basis.card_le_card_of_linearIndependent

added theorem Module.Basis.card_le_card_of_submodule

added def Module.Basis.indexEquiv

added theorem Module.Basis.le_span

added theorem Module.Basis.mk_eq_rank''

added theorem Module.Basis.mk_eq_rank'.{m}

added theorem Module.Basis.mk_eq_rank

added theorem Module.Basis.mk_range_eq_rank

Modified Mathlib/LinearAlgebra/Dual/Basis.lean

deleted theorem Basis.coe_dualBasis

deleted theorem Basis.coe_toDual_self

deleted theorem Basis.coord_toDualEquiv_symm_apply

deleted def Basis.dualBasis

deleted theorem Basis.dualBasis_apply

deleted theorem Basis.dualBasis_apply_self

deleted theorem Basis.dualBasis_coord_toDualEquiv_apply

deleted theorem Basis.dualBasis_equivFun

deleted theorem Basis.dualBasis_repr

deleted theorem Basis.eval_injective

deleted theorem Basis.eval_ker

deleted theorem Basis.eval_range

deleted theorem Basis.linearCombination_coord

deleted theorem Basis.linearCombination_dualBasis

deleted theorem Basis.sum_dual_apply_smul_coord

deleted def Basis.toDual

deleted def Basis.toDualEquiv

deleted theorem Basis.toDualEquiv_apply

deleted def Basis.toDualFlip

deleted theorem Basis.toDualFlip_apply

deleted theorem Basis.toDual_apply

deleted theorem Basis.toDual_apply_left

deleted theorem Basis.toDual_apply_right

deleted theorem Basis.toDual_eq_equivFun

deleted theorem Basis.toDual_eq_repr

deleted theorem Basis.toDual_inj

deleted theorem Basis.toDual_injective

deleted theorem Basis.toDual_ker

deleted theorem Basis.toDual_linearCombination_left

deleted theorem Basis.toDual_linearCombination_right

deleted theorem Basis.toDual_range

deleted theorem Basis.toDual_toDual

added theorem Module.Basis.coe_dualBasis

added theorem Module.Basis.coe_toDual_self

added theorem Module.Basis.coord_toDualEquiv_symm_apply

added def Module.Basis.dualBasis

added theorem Module.Basis.dualBasis_apply

added theorem Module.Basis.dualBasis_apply_self

added theorem Module.Basis.dualBasis_coord_toDualEquiv_apply

added theorem Module.Basis.dualBasis_equivFun

added theorem Module.Basis.dualBasis_repr

added theorem Module.Basis.eval_injective

added theorem Module.Basis.eval_ker

added theorem Module.Basis.eval_range

added theorem Module.Basis.linearCombination_coord

added theorem Module.Basis.linearCombination_dualBasis

added theorem Module.Basis.sum_dual_apply_smul_coord

added def Module.Basis.toDual

added def Module.Basis.toDualEquiv

added theorem Module.Basis.toDualEquiv_apply

added def Module.Basis.toDualFlip

added theorem Module.Basis.toDualFlip_apply

added theorem Module.Basis.toDual_apply

added theorem Module.Basis.toDual_apply_left

added theorem Module.Basis.toDual_apply_right

added theorem Module.Basis.toDual_eq_equivFun

added theorem Module.Basis.toDual_eq_repr

added theorem Module.Basis.toDual_inj

added theorem Module.Basis.toDual_injective

added theorem Module.Basis.toDual_ker

added theorem Module.Basis.toDual_linearCombination_left

added theorem Module.Basis.toDual_linearCombination_right

added theorem Module.Basis.toDual_range

added theorem Module.Basis.toDual_toDual

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

deleted theorem Basis.dual_rank_eq

added theorem Module.Basis.dual_rank_eq

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

deleted theorem Basis.repr_smul'

added theorem Module.Basis.repr_smul'

Modified Mathlib/LinearAlgebra/FreeAlgebra.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

added theorem Module.Basis.repr_algebraMap

deleted theorem Module.Free.Basis.repr_algebraMap

Modified Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Quotient.lean

Modified Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

Modified Mathlib/LinearAlgebra/FreeModule/Int.lean

deleted theorem Basis.SmithNormalForm.toAddSubgroup_index_eq_ite

deleted theorem Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod

deleted theorem Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff

added theorem Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite

added theorem Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod

added theorem Module.Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff

Modified Mathlib/LinearAlgebra/FreeModule/ModN.lean

Modified Mathlib/LinearAlgebra/FreeModule/Norm.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

deleted theorem Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord

deleted theorem Basis.SmithNormalForm.le_ker_coord_of_notMem_range

deleted theorem Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul

deleted theorem Basis.SmithNormalForm.repr_comp_embedding_eq_smul

deleted theorem Basis.SmithNormalForm.repr_eq_zero_of_notMem_range

deleted theorem Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix

deleted structure Basis.SmithNormalForm

added theorem Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord

added theorem Module.Basis.SmithNormalForm.le_ker_coord_of_notMem_range

added theorem Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul

added theorem Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul

added theorem Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range

added theorem Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix

added structure Module.Basis.SmithNormalForm

Modified Mathlib/LinearAlgebra/LinearDisjoint.lean

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

deleted theorem Basis.coePiBasisFun.toMatrix_eq_transpose

deleted def Basis.invertibleToMatrix

deleted theorem Basis.restrictScalars_toMatrix

deleted theorem Basis.sum_toMatrix_smul_self

deleted theorem Basis.toLin_toMatrix

deleted def Basis.toMatrix

deleted def Basis.toMatrixEquiv

deleted theorem Basis.toMatrix_apply

deleted theorem Basis.toMatrix_eq_toMatrix_constr

deleted theorem Basis.toMatrix_isUnitSMul

deleted theorem Basis.toMatrix_map

deleted theorem Basis.toMatrix_map_vecMul

deleted theorem Basis.toMatrix_mulVec_repr

deleted theorem Basis.toMatrix_mul_toMatrix

deleted theorem Basis.toMatrix_mul_toMatrix_flip

deleted theorem Basis.toMatrix_reindex'

deleted theorem Basis.toMatrix_reindex

deleted theorem Basis.toMatrix_self

deleted theorem Basis.toMatrix_smul

deleted theorem Basis.toMatrix_smul_left

deleted theorem Basis.toMatrix_transpose_apply

deleted theorem Basis.toMatrix_unitsSMul

deleted theorem Basis.toMatrix_update

added theorem Module.Basis.coePiBasisFun.toMatrix_eq_transpose

added def Module.Basis.invertibleToMatrix

added theorem Module.Basis.restrictScalars_toMatrix

added theorem Module.Basis.sum_toMatrix_smul_self

added theorem Module.Basis.toLin_toMatrix

added def Module.Basis.toMatrix

added def Module.Basis.toMatrixEquiv

added theorem Module.Basis.toMatrix_apply

added theorem Module.Basis.toMatrix_eq_toMatrix_constr

added theorem Module.Basis.toMatrix_isUnitSMul

added theorem Module.Basis.toMatrix_map

added theorem Module.Basis.toMatrix_map_vecMul

added theorem Module.Basis.toMatrix_mulVec_repr

added theorem Module.Basis.toMatrix_mul_toMatrix

added theorem Module.Basis.toMatrix_mul_toMatrix_flip

added theorem Module.Basis.toMatrix_reindex'

added theorem Module.Basis.toMatrix_reindex

added theorem Module.Basis.toMatrix_self

added theorem Module.Basis.toMatrix_smul

added theorem Module.Basis.toMatrix_smul_left

added theorem Module.Basis.toMatrix_transpose_apply

added theorem Module.Basis.toMatrix_unitsSMul

added theorem Module.Basis.toMatrix_update

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Minpoly.lean

Modified Mathlib/LinearAlgebra/Matrix/Dual.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean

Modified Mathlib/LinearAlgebra/Matrix/LDL.lean

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

Modified Mathlib/LinearAlgebra/Matrix/StdBasis.lean

deleted theorem Basis.matrix_apply

added theorem Module.Basis.matrix_apply

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

deleted theorem Basis.end_apply

deleted theorem Basis.end_apply_apply

deleted def Basis.linearMap

deleted theorem Basis.linearMap_apply

deleted theorem Basis.linearMap_apply_apply

added theorem Module.Basis.end_apply

added theorem Module.Basis.end_apply_apply

added def Module.Basis.linearMap

added theorem Module.Basis.linearMap_apply

added theorem Module.Basis.linearMap_apply_apply

Modified Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basis.lean

deleted theorem Basis.ext_multilinear

added theorem Module.Basis.ext_multilinear

Modified Mathlib/LinearAlgebra/Orientation.lean

deleted theorem Basis.abs_det_adjustToOrientation

deleted def Basis.adjustToOrientation

deleted theorem Basis.adjustToOrientation_apply_eq_or_eq_neg

deleted theorem Basis.det_adjustToOrientation

deleted theorem Basis.map_orientation_eq_det_inv_smul

deleted theorem Basis.orientation_adjustToOrientation

deleted theorem Basis.orientation_comp_linearEquiv_eq_iff_det_pos

deleted theorem Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg

deleted theorem Basis.orientation_eq_iff_det_pos

deleted theorem Basis.orientation_eq_or_eq_neg

deleted theorem Basis.orientation_isEmpty

deleted theorem Basis.orientation_map

deleted theorem Basis.orientation_ne_iff_eq_neg

deleted theorem Basis.orientation_neg_single

deleted theorem Basis.orientation_reindex

deleted theorem Basis.orientation_unitsSMul

added theorem Module.Basis.abs_det_adjustToOrientation

added def Module.Basis.adjustToOrientation

added theorem Module.Basis.adjustToOrientation_apply_eq_or_eq_neg

added theorem Module.Basis.det_adjustToOrientation

added theorem Module.Basis.map_orientation_eq_det_inv_smul

added theorem Module.Basis.orientation_adjustToOrientation

added theorem Module.Basis.orientation_comp_linearEquiv_eq_iff_det_pos

added theorem Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg

added theorem Module.Basis.orientation_eq_iff_det_pos

added theorem Module.Basis.orientation_eq_or_eq_neg

added theorem Module.Basis.orientation_isEmpty

added theorem Module.Basis.orientation_map

added theorem Module.Basis.orientation_ne_iff_eq_neg

added theorem Module.Basis.orientation_neg_single

added theorem Module.Basis.orientation_reindex

added theorem Module.Basis.orientation_unitsSMul

Modified Mathlib/LinearAlgebra/PID.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basis.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Real.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/StdBasis.lean

Modified Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean

deleted def Basis.baseChange

deleted theorem Basis.baseChange_apply

deleted theorem Basis.baseChange_repr_tmul

deleted def Basis.tensorProduct

deleted theorem Basis.tensorProduct_apply'

deleted theorem Basis.tensorProduct_apply

deleted theorem Basis.tensorProduct_repr_tmul_apply

added def Module.Basis.baseChange

added theorem Module.Basis.baseChange_apply

added theorem Module.Basis.baseChange_repr_tmul

added def Module.Basis.tensorProduct

added theorem Module.Basis.tensorProduct_apply'

added theorem Module.Basis.tensorProduct_apply

added theorem Module.Basis.tensorProduct_repr_tmul_apply

Modified Mathlib/LinearAlgebra/TensorProduct/Matrix.lean

Modified Mathlib/MeasureTheory/Group/Defs.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

deleted theorem Basis.addHaar_eq_iff

deleted theorem Basis.addHaar_reindex

deleted theorem Basis.addHaar_self

deleted theorem Basis.coe_parallelepiped

deleted def Basis.parallelepiped

deleted theorem Basis.parallelepiped_map

deleted theorem Basis.parallelepiped_reindex

deleted theorem Basis.prod_addHaar

deleted theorem Basis.prod_parallelepiped

added theorem Module.Basis.addHaar_eq_iff

added theorem Module.Basis.addHaar_reindex

added theorem Module.Basis.addHaar_self

added theorem Module.Basis.coe_parallelepiped

added def Module.Basis.parallelepiped

added theorem Module.Basis.parallelepiped_map

added theorem Module.Basis.parallelepiped_reindex

added theorem Module.Basis.prod_addHaar

added theorem Module.Basis.prod_parallelepiped

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

deleted theorem Basis.map_addHaar

deleted theorem Basis.parallelepiped_basisFun

deleted theorem Basis.parallelepiped_eq_map

added theorem Module.Basis.map_addHaar

added theorem Module.Basis.parallelepiped_basisFun

added theorem Module.Basis.parallelepiped_eq_map

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Defs.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RepresentationTheory/Tannaka.lean

Modified Mathlib/RingTheory/Adjoin/Basic.lean

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/AlgebraTower.lean

deleted theorem Basis.algebraMapCoeffs_apply

deleted theorem Basis.algebraMapCoeffs_repr

deleted theorem Basis.algebraMap_injective

deleted theorem Basis.coe_algebraMapCoeffs

deleted theorem Basis.isScalarTower_finsupp

deleted theorem Basis.isScalarTower_of_nonempty

deleted theorem Basis.smulTower'_apply

deleted theorem Basis.smulTower'_repr

deleted theorem Basis.smulTower'_repr_mk

deleted def Basis.smulTower

deleted theorem Basis.smulTower_apply

deleted theorem Basis.smulTower_repr

deleted theorem Basis.smulTower_repr_mk

added theorem Module.Basis.algebraMapCoeffs_apply

added theorem Module.Basis.algebraMapCoeffs_repr

added theorem Module.Basis.algebraMap_injective

added theorem Module.Basis.coe_algebraMapCoeffs

added theorem Module.Basis.isScalarTower_finsupp

added theorem Module.Basis.isScalarTower_of_nonempty

added theorem Module.Basis.smulTower'_apply

added theorem Module.Basis.smulTower'_repr

added theorem Module.Basis.smulTower'_repr_mk

added def Module.Basis.smulTower

added theorem Module.Basis.smulTower_apply

added theorem Module.Basis.smulTower_repr

added theorem Module.Basis.smulTower_repr_mk

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Extension/Cotangent/Basic.lean

Modified Mathlib/RingTheory/Finiteness/Basic.lean

Modified Mathlib/RingTheory/Finiteness/Defs.lean

Modified Mathlib/RingTheory/FractionalIdeal/Norm.lean

Modified Mathlib/RingTheory/Ideal/Basis.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Kaehler/JacobiZariski.lean

Modified Mathlib/RingTheory/Kaehler/Polynomial.lean

Modified Mathlib/RingTheory/LinearDisjoint.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Localization/Module.lean

deleted theorem Basis.localizationLocalization_apply

deleted theorem Basis.localizationLocalization_repr_algebraMap

deleted theorem Basis.localizationLocalization_span

deleted theorem Basis.ofIsLocalizedModule_apply

deleted theorem Basis.ofIsLocalizedModule_repr_apply

deleted theorem Basis.ofIsLocalizedModule_span

added theorem Module.Basis.localizationLocalization_apply

added theorem Module.Basis.localizationLocalization_repr_algebraMap

added theorem Module.Basis.localizationLocalization_span

added theorem Module.Basis.ofIsLocalizedModule_apply

added theorem Module.Basis.ofIsLocalizedModule_repr_apply

added theorem Module.Basis.ofIsLocalizedModule_span

Modified Mathlib/RingTheory/Localization/NormTrace.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean

Modified Mathlib/RingTheory/NormTrace.lean

Modified Mathlib/RingTheory/Polynomial/DegreeLT.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

Modified Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

Modified Mathlib/RingTheory/TensorProduct/Free.lean

deleted theorem Basis.baseChange_end

deleted theorem Basis.baseChange_linearMap

added theorem Module.Basis.baseChange_end

added theorem Module.Basis.baseChange_linearMap

Modified Mathlib/RingTheory/Trace/Quotient.lean

Modified Mathlib/RingTheory/Unramified/Field.lean

Modified Mathlib/RingTheory/Unramified/Finite.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

deleted theorem Basis.coe_constrL

deleted def Basis.constrL

deleted theorem Basis.constrL_apply

deleted theorem Basis.constrL_basis

deleted def Basis.equivFunL

deleted theorem Basis.equivFunL_symm_apply_repr

added theorem Module.Basis.coe_constrL

added def Module.Basis.constrL

added theorem Module.Basis.constrL_apply

added theorem Module.Basis.constrL_basis

added def Module.Basis.equivFunL

added theorem Module.Basis.equivFunL_symm_apply_repr

Modified Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

Modified docs/overview.yaml

Modified docs/undergrad.yaml