Commit 2024-08-30 00:21 ea3ee6af

View on Github →

chore: rename Finsupp.total (#16277) to Finsupp.linearCombination.

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

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

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/Lie/BaseChange.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

Modified Mathlib/Algebra/Module/Projective.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

deleted theorem DFinsupp.inner_sum

deleted theorem DFinsupp.sum_inner

deleted theorem Finsupp.inner_sum

deleted theorem Finsupp.sum_inner

deleted theorem OrthogonalFamily.inner_sum

deleted theorem Orthonormal.inner_sum

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/PurelyInseparable.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/Basis/Bilinear.lean

Modified Mathlib/LinearAlgebra/Basis/Cardinality.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

modified theorem Basis.coe_repr_symm

added theorem Basis.linearCombination_repr

added theorem Basis.repr_linearCombination

modified theorem Basis.repr_symm_apply

deleted theorem Basis.repr_total

deleted theorem Basis.total_repr

Modified Mathlib/LinearAlgebra/BilinearForm/Hom.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Dual.lean

added theorem Basis.linearCombination_coord

added theorem Basis.linearCombination_dualBasis

added theorem Basis.toDual_linearCombination_left

added theorem Basis.toDual_linearCombination_right

deleted theorem Basis.toDual_total_left

deleted theorem Basis.toDual_total_right

deleted theorem Basis.total_coord

deleted theorem Basis.total_dualBasis

modified theorem Module.DualBases.lc_def

Modified Mathlib/LinearAlgebra/Finsupp.lean

added theorem Finsupp.apply_linearCombination

added theorem Finsupp.apply_linearCombination_id

deleted theorem Finsupp.apply_total

deleted theorem Finsupp.apply_total_id

added def Finsupp.linearCombination

added def Finsupp.linearCombinationOn

added theorem Finsupp.linearCombinationOn_range

added theorem Finsupp.linearCombination_apply

added theorem Finsupp.linearCombination_apply_of_mem_supported

added theorem Finsupp.linearCombination_comapDomain

added theorem Finsupp.linearCombination_comp

added theorem Finsupp.linearCombination_comp_lmapDomain

added theorem Finsupp.linearCombination_embDomain

added theorem Finsupp.linearCombination_eq_fintype_linearCombination

added theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply

added theorem Finsupp.linearCombination_equivMapDomain

added theorem Finsupp.linearCombination_fin_zero

added theorem Finsupp.linearCombination_id_surjective

added theorem Finsupp.linearCombination_linearCombination

added theorem Finsupp.linearCombination_mapDomain

added theorem Finsupp.linearCombination_onFinset

added theorem Finsupp.linearCombination_option

added theorem Finsupp.linearCombination_range

added theorem Finsupp.linearCombination_single

added theorem Finsupp.linearCombination_surjective

added theorem Finsupp.linearCombination_unique

added theorem Finsupp.linearCombination_zero

added theorem Finsupp.linearCombination_zero_apply

added theorem Finsupp.lmapDomain_linearCombination

deleted theorem Finsupp.lmapDomain_total

added theorem Finsupp.mem_span_iff_linearCombination

deleted theorem Finsupp.mem_span_iff_total

added theorem Finsupp.mem_span_image_iff_linearCombination

deleted theorem Finsupp.mem_span_image_iff_total

added theorem Finsupp.range_linearCombination

deleted theorem Finsupp.range_total

added theorem Finsupp.span_eq_range_linearCombination

deleted theorem Finsupp.span_eq_range_total

added theorem Finsupp.span_image_eq_map_linearCombination

deleted theorem Finsupp.span_image_eq_map_total

deleted theorem Finsupp.totalOn_range

deleted theorem Finsupp.total_apply

deleted theorem Finsupp.total_apply_of_mem_supported

deleted theorem Finsupp.total_comapDomain

deleted theorem Finsupp.total_comp

deleted theorem Finsupp.total_comp_lmapDomain

deleted theorem Finsupp.total_embDomain

deleted theorem Finsupp.total_eq_fintype_total

deleted theorem Finsupp.total_eq_fintype_total_apply

deleted theorem Finsupp.total_equivMapDomain

deleted theorem Finsupp.total_fin_zero

deleted theorem Finsupp.total_id_surjective

deleted theorem Finsupp.total_mapDomain

deleted theorem Finsupp.total_onFinset

deleted theorem Finsupp.total_option

deleted theorem Finsupp.total_range

deleted theorem Finsupp.total_single

deleted theorem Finsupp.total_surjective

deleted theorem Finsupp.total_total

deleted theorem Finsupp.total_unique

deleted theorem Finsupp.total_zero

deleted theorem Finsupp.total_zero_apply

added theorem Fintype.linearCombination_apply

added theorem Fintype.linearCombination_apply_single

added theorem Fintype.range_linearCombination

deleted theorem Fintype.range_total

deleted theorem Fintype.total_apply

deleted theorem Fintype.total_apply_single

added theorem LinearMap.map_finsupp_linearCombination

deleted theorem LinearMap.map_finsupp_total

added theorem Span.finsupp_linearCombination_repr

deleted theorem Span.finsupp_total_repr

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/LinearDisjoint.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added def LinearIndependent.linearCombinationEquiv

added theorem LinearIndependent.linearCombinationEquiv_apply_coe

added theorem LinearIndependent.linearCombination_comp_repr

added theorem LinearIndependent.linearCombination_ne_of_not_mem_support

added theorem LinearIndependent.linearCombination_repr

deleted def LinearIndependent.totalEquiv

deleted theorem LinearIndependent.totalEquiv_apply_coe

deleted theorem LinearIndependent.total_comp_repr

deleted theorem LinearIndependent.total_ne_of_not_mem_support

deleted theorem LinearIndependent.total_repr

added theorem linearIndependent_iff_injective_linearCombination

deleted theorem linearIndependent_iff_injective_total

added theorem linearIndependent_iff_linearCombinationOn

deleted theorem linearIndependent_iff_totalOn

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

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

Modified Mathlib/LinearAlgebra/QuadraticForm/Basis.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/Adjoin/Basic.lean

Modified Mathlib/RingTheory/Adjoin/FG.lean

Modified Mathlib/RingTheory/AlgebraicIndependent.lean

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/Kaehler/Basic.lean

added theorem KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination

deleted theorem KaehlerDifferential.derivationQuotKerTotal_lift_comp_total

added theorem KaehlerDifferential.linearCombination_surjective

deleted theorem KaehlerDifferential.total_surjective

Modified Mathlib/RingTheory/Kaehler/Polynomial.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

Modified Mathlib/RingTheory/Noetherian.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/RingHom/FinitePresentation.lean

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

Modified Mathlib/RingTheory/RingHom/Surjective.lean

Modified Mathlib/RingTheory/SimpleModule.lean

Modified Mathlib/RingTheory/Unramified/Finite.lean

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