Commit 2025-04-22 08:56 4d71f1a6

View on Github →

feat: ι →₀ R is a finite R-module iff ι is finite (#23997)

Estimated changes

Modified Mathlib/Data/Finsupp/Single.lean

added theorem Finsupp.apply_surjective

Modified Mathlib/Data/Matrix/Rank.lean

Modified Mathlib/LinearAlgebra/Basis/Cardinality.lean

modified theorem basis_finite_of_finite_spans

added theorem finite_of_span_finite_eq_top_finsupp

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

added theorem Module.finite_finsupp_iff

added theorem Module.finite_finsupp_self_iff

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

added theorem Finsupp.span_le_supported_biUnion_support

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

modified theorem Finsupp.linearIndependent_single

added theorem Finsupp.linearIndependent_single_iff

added theorem Finsupp.linearIndependent_single_of_ne_zero

added theorem Finsupp.linearIndependent_single_one

Modified Mathlib/LinearAlgebra/StdBasis.lean

added theorem Pi.linearIndependent_single_of_ne_zero

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean