doc-next-gen

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Module docstring

{"# Lemmas about rank and finrank in rings satisfying strong rank condition.

Main statements

For modules over rings satisfying the rank condition

  • Basis.le_span: the cardinality of a basis is bounded by the cardinality of any spanning set

For modules over rings satisfying the strong rank condition

  • linearIndependent_le_span: For any linearly independent family v : ι → M and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.
  • linearIndependent_le_basis: If b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

For modules over rings with invariant basis number (including all commutative rings and all noetherian rings)

  • mk_eq_mk_of_basis: the dimension theorem, any two bases of the same vector space have the same cardinality.

Additional definition

  • Algebra.IsQuadraticExtension: An extension of rings R ⊆ S is quadratic if S is a free R-algebra of rank 2.

"}

mk_eq_mk_of_basis theorem
(v : Basis ι R M) (v' : Basis ι' R M) : Cardinal.lift.{w'} #ι = Cardinal.lift.{w} #ι'
Full source 
/-- The dimension theorem: if `v` and `v'` are two bases, their index types
have the same cardinalities. -/
theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) :
    Cardinal.lift.{w'} #ι = Cardinal.lift.{w} #ι' := by
  classical
  haveI := nontrivial_of_invariantBasisNumber R
  cases fintypeOrInfinite ι
  · -- `v` is a finite basis, so by `basis_finite_of_finite_spans` so is `v'`.
    -- haveI : Finite (range v) := Set.finite_range v
    haveI := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
    cases nonempty_fintype ι'
    -- We clean up a little:
    rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
    simp only [Cardinal.lift_natCast, Nat.cast_inj]
    -- Now we can use invariant basis number to show they have the same cardinality.
    apply card_eq_of_linearEquiv R
    exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr(Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'
  · -- `v` is an infinite basis,
    -- so by `infinite_basis_le_maximal_linearIndependent`, `v'` is at least as big,
    -- and then applying `infinite_basis_le_maximal_linearIndependent` again
    -- we see they have the same cardinality.
    have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
    rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩
    haveI : Infinite ι' := Infinite.of_injective f f.2
    have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
    exact le_antisymm w₁ w₂
Dimension Theorem: Cardinality of Basis Index Sets in Modules over Rings with Invariant Basis Number
Informal description
Let $R$ be a ring with the invariant basis number property, and let $M$ be an $R$-module. If $v : \iota \to M$ and $v' : \iota' \to M$ are two bases for $M$, then the cardinalities of the index sets $\iota$ and $\iota'$ are equal, i.e., $|\iota| = |\iota'|$.
Basis.indexEquiv definition
(v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι'
Full source 
/-- Given two bases indexed by `ι` and `ι'` of an `R`-module, where `R` satisfies the invariant
basis number property, an equiv `ι ≃ ι'`. -/
def Basis.indexEquiv (v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι' :=
  (Cardinal.lift_mk_eq'.1 <| mk_eq_mk_of_basis v v').some
Equivalence of Basis Index Sets under Invariant Basis Number Property
Informal description
Given two bases $v : \iota \to M$ and $v' : \iota' \to M$ of an $R$-module $M$, where $R$ satisfies the invariant basis number property, there exists an equivalence (bijection) between the index sets $\iota$ and $\iota'$.
mk_eq_mk_of_basis' theorem
{ι' : Type w} (v : Basis ι R M) (v' : Basis ι' R M) : #ι = #ι'
Full source 
theorem mk_eq_mk_of_basis' {ι' : Type w} (v : Basis ι R M) (v' : Basis ι' R M) : #ι = #ι' :=
  Cardinal.lift_inj.1 <| mk_eq_mk_of_basis v v'
Dimension Theorem: Equality of Basis Cardinalities in Modules over Rings with Invariant Basis Number
Informal description
Let $R$ be a ring with the invariant basis number property, and let $M$ be an $R$-module. Given two bases $v : \iota \to M$ and $v' : \iota' \to M$ of $M$, the cardinality of the index set $\iota$ is equal to the cardinality of the index set $\iota'$, i.e., $|\iota| = |\iota'|$.
Basis.le_span'' theorem
{ι : Type*} [Fintype ι] (b : Basis ι R M) {w : Set M} [Fintype w] (s : span R w = ⊤) : Fintype.card ι ≤ Fintype.card w
Full source 
/-- An auxiliary lemma for `Basis.le_span`.

If `R` satisfies the rank condition,
then for any finite basis `b : Basis ι R M`,
and any finite spanning set `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem Basis.le_span'' {ι : Type*} [Fintype ι] (b : Basis ι R M) {w : Set M} [Fintype w]
    (s : span R w = ⊤) : Fintype.card ι ≤ Fintype.card w := by
  -- We construct a surjective linear map `(w → R) →ₗ[R] (ι → R)`,
  -- by expressing a linear combination in `w` as a linear combination in `ι`.
  fapply card_le_of_surjective' R
  · exact b.repr.toLinearMap.comp (Finsupp.linearCombination R (↑))
  · apply Surjective.comp (g := b.repr.toLinearMap)
    · apply LinearEquiv.surjective
    rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
    simpa using s
Cardinality Bound of Basis by Spanning Set in Rank Condition Rings
Informal description
Let $R$ be a ring satisfying the rank condition, $M$ an $R$-module, and $b : \iota \to M$ a finite basis for $M$ (where $\iota$ is a finite type). For any finite spanning set $w \subseteq M$ (i.e., $\text{span}_R w = M$), the cardinality of $\iota$ is less than or equal to the cardinality of $w$.
basis_le_span' theorem
{ι : Type*} (b : Basis ι R M) {w : Set M} [Fintype w] (s : span R w = ⊤) : #ι ≤ Fintype.card w
Full source 
/--
Another auxiliary lemma for `Basis.le_span`, which does not require assuming the basis is finite,
but still assumes we have a finite spanning set.
-/
theorem basis_le_span' {ι : Type*} (b : Basis ι R M) {w : Set M} [Fintype w] (s : span R w = ⊤) :
    #ι ≤ Fintype.card w := by
  haveI := nontrivial_of_invariantBasisNumber R
  haveI := basis_finite_of_finite_spans w.toFinite s b
  cases nonempty_fintype ι
  rw [Cardinal.mk_fintype ι]
  simp only [Nat.cast_le]
  exact Basis.le_span'' b s
Cardinality Bound of Basis by Finite Spanning Set in Rank Condition Rings
Informal description
Let $R$ be a ring satisfying the rank condition, $M$ an $R$-module, and $b \colon \iota \to M$ a basis for $M$. For any finite spanning set $w \subseteq M$ (i.e., $\text{span}_R w = M$), the cardinality of $\iota$ is less than or equal to the cardinality of $w$.
Basis.le_span theorem
{J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤) : #(range v) ≤ #J
Full source 
/-- If `R` satisfies the rank condition,
then the cardinality of any basis is bounded by the cardinality of any spanning set.
-/
theorem Basis.le_span {J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤) : #(range v) ≤ #J := by
  haveI := nontrivial_of_invariantBasisNumber R
  cases fintypeOrInfinite J
  · rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
    convert Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
    simp
  · let S : J → Set ι := fun j => ↑(v.repr j).support
    let S' : J → Set M := fun j => v '' S j
    have hs : rangerange v ⊆ ⋃ j, S' j := by
      intro b hb
      rcases mem_range.1 hb with ⟨i, hi⟩
      have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
      rw [hJ] at this
      replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single_ne_zero _ one_ne_zero] at this
      · subst b
        rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
        exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
    refine le_of_not_lt fun IJ => ?_
    suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_lt this ⟨Set.embeddingOfSubset _ _ hs⟩
    refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
    · exact fun j => (Cardinal.lt_aleph0_of_finite _).le
    · simpa
Cardinality Bound of Basis by Spanning Set in Rank Condition Rings
Informal description
Let $R$ be a ring satisfying the rank condition, $M$ an $R$-module, and $v \colon \iota \to M$ a basis for $M$. For any spanning set $J \subseteq M$ (i.e., $\text{span}_R J = M$), the cardinality of the range of $v$ is less than or equal to the cardinality of $J$.
linearIndependent_le_span_aux' theorem
{ι : Type*} [Fintype ι] (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype w] (s : range v ≤ span R w) : Fintype.card ι ≤ Fintype.card w
Full source 
theorem linearIndependent_le_span_aux' {ι : Type*} [Fintype ι] (v : ι → M)
    (i : LinearIndependent R v) (w : Set M) [Fintype w] (s : range v ≤ span R w) :
    Fintype.card ι ≤ Fintype.card w := by
  -- We construct an injective linear map `(ι → R) →ₗ[R] (w → R)`,
  -- by thinking of `f : ι → R` as a linear combination of the finite family `v`,
  -- and expressing that (using the axiom of choice) as a linear combination over `w`.
  -- We can do this linearly by constructing the map on a basis.
  fapply card_le_of_injective' R
  · apply Finsupp.linearCombination
    exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩
  · intro f g h
    apply_fun linearCombination R ((↑) : w → M) at h
    simp only [linearCombination_linearCombination, Submodule.coe_mk,
               Span.finsupp_linearCombination_repr] at h
    exact i h
Cardinality Bound for Linearly Independent Families in Modules with Finite Spanning Sets
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module. For any finite index type $\iota$ and any linearly independent family $v \colon \iota \to M$, if there exists a finite spanning set $w \subseteq M$ such that the range of $v$ is contained in the span of $w$, then the cardinality of $\iota$ is less than or equal to the cardinality of $w$.
LinearIndependent.finite_of_le_span_finite theorem
{ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Finite w] (s : range v ≤ span R w) : Finite ι
Full source 
/-- If `R` satisfies the strong rank condition,
then any linearly independent family `v : ι → M`
contained in the span of some finite `w : Set M`,
is itself finite.
-/
lemma LinearIndependent.finite_of_le_span_finite {ι : Type*} (v : ι → M) (i : LinearIndependent R v)
    (w : Set M) [Finite w] (s : range v ≤ span R w) : Finite ι :=
  letI := Fintype.ofFinite w
  Fintype.finite <| fintypeOfFinsetCardLe (Fintype.card w) fun t => by
    let v' := fun x : (t : Set ι) => v x
    have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
    have s' : range v' ≤ span R w := (range_comp_subset_range _ _).trans s
    simpa using linearIndependent_le_span_aux' v' i' w s'
Finiteness of Linearly Independent Families in Finite Spanning Sets
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module. For any linearly independent family $v \colon \iota \to M$ in $M$, if there exists a finite set $w \subseteq M$ such that the range of $v$ is contained in the span of $w$, then the index set $\iota$ is finite.
linearIndependent_le_span' theorem
{ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype w] (s : range v ≤ span R w) : #ι ≤ Fintype.card w
Full source 
/-- If `R` satisfies the strong rank condition,
then for any linearly independent family `v : ι → M`
contained in the span of some finite `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem linearIndependent_le_span' {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M)
    [Fintype w] (s : range v ≤ span R w) : #ι ≤ Fintype.card w := by
  haveI : Finite ι := i.finite_of_le_span_finite v w s
  letI := Fintype.ofFinite ι
  rw [Cardinal.mk_fintype]
  simp only [Nat.cast_le]
  exact linearIndependent_le_span_aux' v i w s
Cardinality Bound for Linearly Independent Families in Finite Spanning Sets
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module. For any linearly independent family $v \colon \iota \to M$ and any finite spanning set $w \subseteq M$ such that the range of $v$ is contained in the span of $w$, the cardinality of $\iota$ is bounded by the cardinality of $w$, i.e., $|\iota| \leq |w|$.
linearIndependent_le_span theorem
{ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype w] (s : span R w = ⊤) : #ι ≤ Fintype.card w
Full source 
/-- If `R` satisfies the strong rank condition,
then for any linearly independent family `v : ι → M`
and any finite spanning set `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem linearIndependent_le_span {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M)
    [Fintype w] (s : span R w = ⊤) : #ι ≤ Fintype.card w := by
  apply linearIndependent_le_span' v i w
  rw [s]
  exact le_top
Cardinality Bound for Linearly Independent Sets in Finitely Spanned Modules
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module. For any linearly independent family of vectors $\{v_i\}_{i \in \iota}$ in $M$ and any finite spanning set $w \subseteq M$ (i.e., $\text{span}_R(w) = M$), the cardinality of $\iota$ is bounded by the cardinality of $w$, i.e., $|\iota| \leq |w|$.
linearIndependent_le_span_finset theorem
{ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Finset M) (s : span R (w : Set M) = ⊤) : #ι ≤ w.card
Full source 
/-- A version of `linearIndependent_le_span` for `Finset`. -/
theorem linearIndependent_le_span_finset {ι : Type*} (v : ι → M) (i : LinearIndependent R v)
    (w : Finset M) (s : span R (w : Set M) = ⊤) : #ι ≤ w.card := by
  simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s
Cardinality Bound for Linearly Independent Families in Finitely Spanned Modules (Finset Version)
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module. For any linearly independent family of vectors $\{v_i\}_{i \in \iota}$ in $M$ and any finite spanning set $w \subseteq M$ given as a finset (i.e., $\text{span}_R(w) = M$), the cardinality of $\iota$ is bounded by the size of $w$, i.e., $|\iota| \leq |w|$.
linearIndependent_le_infinite_basis theorem
{ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) : #κ ≤ #ι
Full source 
/-- An auxiliary lemma for `linearIndependent_le_basis`:
we handle the case where the basis `b` is infinite.
-/
theorem linearIndependent_le_infinite_basis {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w}
    (v : κ → M) (i : LinearIndependent R v) : #κ ≤ #ι := by
  classical
  by_contra h
  rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
  let Φ := fun k : κ => (b.repr (v k)).support
  obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber Φ h (by infer_instance)
  let v' := fun k : Φ ⁻¹' {s} => v k
  have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
  have w' : Finite (Φ ⁻¹' {s}) := by
    apply i'.finite_of_le_span_finite v' (s.image b)
    rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
    simp only [SetLike.mem_coe, Subtype.coe_mk, Finset.coe_image]
    apply Basis.mem_span_repr_support
  exact w.false
Cardinality Bound for Linearly Independent Sets in Modules with Infinite Basis
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module with an infinite basis $\{b_i\}_{i \in \iota}$. For any linearly independent family $\{v_k\}_{k \in \kappa}$ in $M$, the cardinality of $\kappa$ is at most the cardinality of $\iota$.
linearIndependent_le_basis theorem
{ι : Type w} (b : Basis ι R M) {κ : Type w} (v : κ → M) (i : LinearIndependent R v) : #κ ≤ #ι
Full source 
/-- Over any ring `R` satisfying the strong rank condition,
if `b` is a basis for a module `M`,
and `s` is a linearly independent set,
then the cardinality of `s` is bounded by the cardinality of `b`.
-/
theorem linearIndependent_le_basis {ι : Type w} (b : Basis ι R M) {κ : Type w} (v : κ → M)
    (i : LinearIndependent R v) : #κ ≤ #ι := by
  classical
  -- We split into cases depending on whether `ι` is infinite.
  cases fintypeOrInfinite ι
  · rw [Cardinal.mk_fintype ι] -- When `ι` is finite, we have `linearIndependent_le_span`,
    haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
    rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]
    exact linearIndependent_le_span v i (range b) b.span_eq
  · -- and otherwise we have `linearIndependent_le_infinite_basis`.
    exact linearIndependent_le_infinite_basis b v i
Cardinality Bound for Linearly Independent Sets Relative to a Basis
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module with a basis $\{b_i\}_{i \in \iota}$. For any linearly independent family of vectors $\{v_k\}_{k \in \kappa}$ in $M$, the cardinality of $\kappa$ is at most the cardinality of $\iota$, i.e., $|\kappa| \leq |\iota|$.
card_le_of_injective'' theorem
{α : Type v} {β : Type v} (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Injective f) : #α ≤ #β
Full source 
/-- `StrongRankCondition` implies that if there is an injective linear map `(α →₀ R) →ₗ[R] β →₀ R`,
then the cardinal of `α` is smaller than or equal to the cardinal of `β`.
-/
theorem card_le_of_injective'' {α : Type v} {β : Type v} (f : (α →₀ R) →ₗ[R] β →₀ R)
    (i : Injective f) : #α ≤ #β := by
  let b : Basis β R (β →₀ R) := ⟨1⟩
  apply linearIndependent_le_basis b (fun (i : α) ↦ f (Finsupp.single i 1))
  rw [LinearIndependent]
  have : (linearCombination R fun i ↦ f (Finsupp.single i 1)) = f := by ext a b; simp
  exact this.symm ▸ i
Cardinality Bound for Injective Linear Maps on Finitely Supported Functions
Informal description
Let $R$ be a ring satisfying the strong rank condition. For any injective linear map $f \colon (\alpha \to_{\text{f}} R) \to_{R} (\beta \to_{\text{f}} R)$ between finitely supported function spaces, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $|\alpha| \leq |\beta|$.
linearIndependent_le_span'' theorem
{ι : Type v} {v : ι → M} (i : LinearIndependent R v) (w : Set M) (s : span R w = ⊤) : #ι ≤ #w
Full source 
/-- If `R` satisfies the strong rank condition, then for any linearly independent family `v : ι → M`
and spanning set `w : Set M`, the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem linearIndependent_le_span'' {ι : Type v} {v : ι → M} (i : LinearIndependent R v) (w : Set M)
    (s : span R w = ⊤) : #ι ≤ #w := by
  fapply card_le_of_injective'' (R := R)
  · apply Finsupp.linearCombination
    exact fun i ↦ Span.repr R w ⟨v i, s ▸ trivial⟩
  · intro f g h
    apply_fun linearCombination R ((↑) : w → M) at h
    simp only [linearCombination_linearCombination, Submodule.coe_mk,
               Span.finsupp_linearCombination_repr] at h
    exact i h
Cardinality Bound for Linearly Independent Sets Relative to Spanning Sets
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module. For any linearly independent family of vectors $\{v_i\}_{i \in \iota}$ in $M$ and any spanning set $w \subseteq M$, the cardinality of $\iota$ is bounded by the cardinality of $w$, i.e., $|\iota| \leq |w|$.
Basis.card_le_card_of_linearIndependent_aux theorem
{R : Type*} [Semiring R] [StrongRankCondition R] (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n
Full source 
/-- Let `R` satisfy the strong rank condition. If `m` elements of a free rank `n` `R`-module are
linearly independent, then `m ≤ n`. -/
theorem Basis.card_le_card_of_linearIndependent_aux {R : Type*} [Semiring R] [StrongRankCondition R]
    (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n := fun h => by
  simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h
Cardinality Bound for Linearly Independent Families in Finite Free Modules
Informal description
Let $R$ be a semiring satisfying the strong rank condition. For any natural numbers $n$ and $m$, and any linearly independent family of vectors $\{v_i\}_{i \in \text{Fin } m}$ in the free $R$-module $\text{Fin } n \to R$, we have $m \leq n$.
maximal_linearIndependent_eq_infinite_basis theorem
{ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : #κ = #ι
Full source 
/-- Over any ring `R` satisfying the strong rank condition,
if `b` is an infinite basis for a module `M`,
then every maximal linearly independent set has the same cardinality as `b`.

This proof (along with some of the lemmas above) comes from
[Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]
-/
theorem maximal_linearIndependent_eq_infinite_basis {ι : Type w} (b : Basis ι R M) [Infinite ι]
    {κ : Type w} (v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : #κ = #ι := by
  apply le_antisymm
  · exact linearIndependent_le_basis b v i
  · haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
    exact infinite_basis_le_maximal_linearIndependent b v i m
Cardinality of Maximal Linearly Independent Sets Equals Basis Cardinality for Infinite Bases
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module with an infinite basis $\{b_i\}_{i \in \iota}$. For any maximal linearly independent family of vectors $\{v_k\}_{k \in \kappa}$ in $M$, the cardinality of $\kappa$ equals the cardinality of $\iota$, i.e., $|\kappa| = |\iota|$.
Basis.mk_eq_rank'' theorem
{ι : Type v} (v : Basis ι R M) : #ι = Module.rank R M
Full source 
theorem Basis.mk_eq_rank'' {ι : Type v} (v : Basis ι R M) : #ι = Module.rank R M := by
  haveI := nontrivial_of_invariantBasisNumber R
  rw [Module.rank_def]
  apply le_antisymm
  · trans
    swap
    · apply le_ciSup (Cardinal.bddAbove_range _)
      exact
        ⟨Set.range v, by
          rw [LinearIndepOn]
          convert v.reindexRange.linearIndependent
          simp⟩
    · exact (Cardinal.mk_range_eq v v.injective).ge
  · apply ciSup_le'
    rintro ⟨s, li⟩
    apply linearIndependent_le_basis v _ li
Cardinality of Basis Equals Module Rank
Informal description
For any basis $\{v_i\}_{i \in \iota}$ of an $R$-module $M$, the cardinality of $\iota$ equals the rank of $M$ over $R$, i.e., $|\iota| = \text{rank}_R(M)$.
Basis.mk_range_eq_rank theorem
(v : Basis ι R M) : #(range v) = Module.rank R M
Full source 
theorem Basis.mk_range_eq_rank (v : Basis ι R M) : #(range v) = Module.rank R M :=
  v.reindexRange.mk_eq_rank''
Cardinality of Basis Range Equals Module Rank
Informal description
For any basis $v : \iota \to M$ of an $R$-module $M$, the cardinality of the range of $v$ equals the rank of $M$ over $R$, i.e., $|\text{range}(v)| = \text{rank}_R(M)$.
rank_eq_card_basis theorem
{ι : Type w} [Fintype ι] (h : Basis ι R M) : Module.rank R M = Fintype.card ι
Full source 
/-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
cardinality of the basis. -/
theorem rank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) :
    Module.rank R M = Fintype.card ι := by
  classical
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]
Rank Equals Cardinality of Basis for Finite-Dimensional Modules
Informal description
Let $M$ be a module over a ring $R$ with a finite basis $\{v_i\}_{i \in \iota}$. Then the rank of $M$ over $R$ is equal to the cardinality of the index set $\iota$, i.e., $\text{rank}_R(M) = |\iota|$.
Basis.card_le_card_of_linearIndependent theorem
{ι : Type*} [Fintype ι] (b : Basis ι R M) {ι' : Type*} [Fintype ι'] {v : ι' → M} (hv : LinearIndependent R v) : Fintype.card ι' ≤ Fintype.card ι
Full source 
theorem Basis.card_le_card_of_linearIndependent {ι : Type*} [Fintype ι] (b : Basis ι R M)
    {ι' : Type*} [Fintype ι'] {v : ι' → M} (hv : LinearIndependent R v) :
    Fintype.card ι' ≤ Fintype.card ι := by
  letI := nontrivial_of_invariantBasisNumber R
  simpa [rank_eq_card_basis b, Cardinal.mk_fintype] using hv.cardinal_lift_le_rank
Cardinality of Linearly Independent Family Bounded by Basis Size
Informal description
Let $M$ be a module over a ring $R$ with a finite basis $\{b_i\}_{i \in \iota}$ indexed by a finite type $\iota$. For any finite linearly independent family $\{v_j\}_{j \in \iota'}$ in $M$ indexed by a finite type $\iota'$, the cardinality of $\iota'$ is less than or equal to the cardinality of $\iota$, i.e., $|\iota'| \leq |\iota|$.
Basis.card_le_card_of_submodule theorem
(N : Submodule R M) [Fintype ι] (b : Basis ι R M) [Fintype ι'] (b' : Basis ι' R N) : Fintype.card ι' ≤ Fintype.card ι
Full source 
theorem Basis.card_le_card_of_submodule (N : Submodule R M) [Fintype ι] (b : Basis ι R M)
    [Fintype ι'] (b' : Basis ι' R N) : Fintype.card ι' ≤ Fintype.card ι :=
  b.card_le_card_of_linearIndependent
    (b'.linearIndependent.map_injOn N.subtype N.injective_subtype.injOn)
Submodule Basis Cardinality Bounded by Module Basis Cardinality
Informal description
Let $M$ be a module over a ring $R$ with a finite basis $\{b_i\}_{i \in \iota}$ indexed by a finite type $\iota$, and let $N$ be a submodule of $M$ with a finite basis $\{b'_j\}_{j \in \iota'}$ indexed by a finite type $\iota'$. Then the cardinality of $\iota'$ is less than or equal to the cardinality of $\iota$, i.e., $|\iota'| \leq |\iota|$.
Basis.card_le_card_of_le theorem
{N O : Submodule R M} (hNO : N ≤ O) [Fintype ι] (b : Basis ι R O) [Fintype ι'] (b' : Basis ι' R N) : Fintype.card ι' ≤ Fintype.card ι
Full source 
theorem Basis.card_le_card_of_le {N O : Submodule R M} (hNO : N ≤ O) [Fintype ι] (b : Basis ι R O)
    [Fintype ι'] (b' : Basis ι' R N) : Fintype.card ι' ≤ Fintype.card ι :=
  b.card_le_card_of_linearIndependent
    (b'.linearIndependent.map_injOn (inclusion hNO) (N.inclusion_injective _).injOn)
Cardinality of Basis for Submodule Bounded by Basis for Containing Module
Informal description
Let $M$ be a module over a ring $R$, and let $N$ and $O$ be submodules of $M$ such that $N \subseteq O$. Suppose $O$ has a finite basis $\{b_i\}_{i \in \iota}$ and $N$ has a finite basis $\{b'_j\}_{j \in \iota'}$. Then the cardinality of $\iota'$ is less than or equal to the cardinality of $\iota$, i.e., $|\iota'| \leq |\iota|$.
Basis.mk_eq_rank theorem
(v : Basis ι R M) : Cardinal.lift.{v} #ι = Cardinal.lift.{w} (Module.rank R M)
Full source 
theorem Basis.mk_eq_rank (v : Basis ι R M) :
    Cardinal.lift.{v} #ι = Cardinal.lift.{w} (Module.rank R M) := by
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]
Cardinality of Basis Index Set Equals Module Rank (Universe-Lifted Version)
Informal description
For any basis $v : \iota \to M$ of an $R$-module $M$, the cardinality of the index set $\iota$ (lifted to a suitable universe) is equal to the rank of $M$ over $R$ (also lifted to a suitable universe). That is, $\text{lift}(\#\iota) = \text{lift}(\text{rank}_R(M))$.
Basis.mk_eq_rank' theorem
(v : Basis ι R M) : Cardinal.lift.{max v m} #ι = Cardinal.lift.{max w m} (Module.rank R M)
Full source 
theorem Basis.mk_eq_rank'.{m} (v : Basis ι R M) :
    Cardinal.lift.{max v m} #ι = Cardinal.lift.{max w m} (Module.rank R M) :=
  Cardinal.lift_umax_eq.{w, v, m}.mpr v.mk_eq_rank
Universe-Lifted Equality of Basis Cardinality and Module Rank
Informal description
For any basis $v : \iota \to M$ of an $R$-module $M$, the cardinality of the index set $\iota$ (lifted to a suitable universe) is equal to the rank of $M$ over $R$ (also lifted to a suitable universe). That is, $\text{lift}(\#\iota) = \text{lift}(\text{rank}_R(M))$, where the lifts are taken to the universe $\max(v, m)$ for $\iota$ and $\max(w, m)$ for the rank.
rank_span theorem
{v : ι → M} (hv : LinearIndependent R v) : Module.rank R ↑(span R (range v)) = #(range v)
Full source 
theorem rank_span {v : ι → M} (hv : LinearIndependent R v) :
    Module.rank R ↑(span R (range v)) = #(range v) := by
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]
Rank of Span Equals Cardinality of Range for Linearly Independent Vectors
Informal description
For any linearly independent family of vectors $v : \iota \to M$ in an $R$-module $M$, the rank of the submodule spanned by the range of $v$ is equal to the cardinality of the range of $v$. That is, $\text{rank}_R(\text{span}_R(\text{range}(v))) = \#(\text{range}(v))$.
rank_span_set theorem
{s : Set M} (hs : LinearIndepOn R id s) : Module.rank R ↑(span R s) = #s
Full source 
theorem rank_span_set {s : Set M} (hs : LinearIndepOn R id s) : Module.rank R ↑(span R s) = #s := by
  rw [← @setOf_mem_eq _ s, ← Subtype.range_coe_subtype]
  exact rank_span hs
Rank of Span Equals Cardinality for Linearly Independent Sets
Informal description
For any subset $s$ of an $R$-module $M$ such that $s$ is linearly independent (with respect to the identity map), the rank of the submodule spanned by $s$ is equal to the cardinality of $s$. That is, $\text{rank}_R(\text{span}_R(s)) = \#s$.
toENat_rank_span_set theorem
{v : ι → M} {s : Set ι} (hs : LinearIndepOn R v s) : (Module.rank R <| span R <| v '' s).toENat = s.encard
Full source 
theorem toENat_rank_span_set {v : ι → M} {s : Set ι} (hs : LinearIndepOn R v s) :
    (Module.rank R <| span R <| v '' s).toENat = s.encard := by
  rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]
Extended Natural Rank of Span Equals Extended Cardinality for Linearly Independent Sets
Informal description
For any family of vectors $v : \iota \to M$ in an $R$-module $M$ and any subset $s \subseteq \iota$ such that the restriction $v|_s$ is linearly independent, the extended natural number rank of the submodule spanned by $v(s)$ is equal to the extended cardinality of $s$. That is, $\text{rank}_R(\text{span}_R(v(s))).\text{toENat} = \text{encard}(s)$.
Submodule.inductionOnRank definition
{R M} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [IsDomain R] [Finite ι] (b : Basis ι R M) (P : Submodule R M → Sort*) (ih : ∀ N : Submodule R M, (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N) (N : Submodule R M) : P N
Full source 
/-- An induction (and recursion) principle for proving results about all submodules of a fixed
finite free module `M`. A property is true for all submodules of `M` if it satisfies the following
"inductive step": the property is true for a submodule `N` if it's true for all submodules `N'`
of `N` with the property that there exists `0 ≠ x ∈ N` such that the sum `N' + Rx` is direct. -/
def Submodule.inductionOnRank {R M} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M]
    [IsDomain R] [Finite ι] (b : Basis ι R M) (P : Submodule R M → Sort*)
    (ih : ∀ N : Submodule R M,
      (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N)
    (N : Submodule R M) : P N :=
  letI := Fintype.ofFinite ι
  Submodule.inductionOnRankAux b P ih (Fintype.card ι) N fun hs hli => by
    simpa using b.card_le_card_of_linearIndependent hli
Rank Induction Principle for Submodules
Informal description
Given a finite free module \( M \) over a ring \( R \) satisfying the strong rank condition, and a property \( P \) of submodules of \( M \), the property \( P \) holds for all submodules of \( M \) if it satisfies the following inductive step: for any submodule \( N \) of \( M \), if \( P \) holds for all submodules \( N' \) of \( N \) such that there exists a nonzero element \( x \in N \) with the sum \( N' + Rx \) being direct, then \( P \) holds for \( N \).
Ideal.rank_eq theorem
{R S : Type*} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S] [Algebra R S] {n m : Type*} [Fintype n] [Fintype m] (b : Basis n R S) {I : Ideal S} (hI : I ≠ ⊥) (c : Basis m R I) : Fintype.card m = Fintype.card n
Full source 
/-- If `S` a module-finite free `R`-algebra, then the `R`-rank of a nonzero `R`-free
ideal `I` of `S` is the same as the rank of `S`. -/
theorem Ideal.rank_eq {R S : Type*} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S]
    [Algebra R S] {n m : Type*} [Fintype n] [Fintype m] (b : Basis n R S) {I : Ideal S}
    (hI : I ≠ ⊥) (c : Basis m R I) : Fintype.card m = Fintype.card n := by
  obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr hI)
  have : LinearIndependent R fun i => b i • a := by
    have hb := b.linearIndependent
    rw [Fintype.linearIndependent_iff] at hb ⊢
    intro g hg
    apply hb g
    simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
    exact hg.resolve_right ha
  exact le_antisymm
    (b.card_le_card_of_linearIndependent (c.linearIndependent.map' (Submodule.subtype I)
      ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
    (c.card_le_card_of_linearIndependent this)
Rank Equality for Nonzero Ideals in Module-Finite Algebras
Informal description
Let $R$ be a commutative ring satisfying the strong rank condition, and let $S$ be a domain with an $R$-algebra structure. Given a finite basis $\{b_i\}_{i \in n}$ for $S$ as an $R$-module and a nonzero ideal $I$ of $S$ with a finite basis $\{c_j\}_{j \in m}$ as an $R$-module, the cardinality of $m$ is equal to the cardinality of $n$, i.e., $|m| = |n|$.
Module.finrank_eq_nat_card_basis theorem
(h : Basis ι R M) : finrank R M = Nat.card ι
Full source 
theorem finrank_eq_nat_card_basis (h : Basis ι R M) :
    finrank R M = Nat.card ι := by
  rw [Nat.card, ← toNat_lifttoNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]
Finite Rank Equals Basis Cardinality for Modules
Informal description
For any basis $h : \iota \to M$ of an $R$-module $M$, the finite rank of $M$ over $R$ is equal to the cardinality of the index set $\iota$ as a natural number. That is, $\text{finrank}_R(M) = \text{Nat.card}(\iota)$.
Module.finrank_eq_card_basis theorem
{ι : Type w} [Fintype ι] (h : Basis ι R M) : finrank R M = Fintype.card ι
Full source 
/-- If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis. -/
theorem finrank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) :
    finrank R M = Fintype.card ι :=
  finrank_eq_of_rank_eq (rank_eq_card_basis h)
Finite Rank Equals Basis Cardinality for Finite-Dimensional Modules
Informal description
Let $M$ be a finite-dimensional module over a ring $R$ with a finite basis $\{v_i\}_{i \in \iota}$. Then the finite rank of $M$ over $R$ is equal to the cardinality of the index set $\iota$, i.e., $\text{finrank}_R(M) = |\iota|$.
Module.mk_finrank_eq_card_basis theorem
[Module.Finite R M] {ι : Type w} (h : Basis ι R M) : (finrank R M : Cardinal.{w}) = #ι
Full source 
/-- If a free module is of finite rank, then the cardinality of any basis is equal to its
`finrank`. -/
theorem mk_finrank_eq_card_basis [Module.Finite R M] {ι : Type w} (h : Basis ι R M) :
    (finrank R M : CardinalCardinal.{w}) = #ι := by
  cases @nonempty_fintype _ (Module.Finite.finite_basis h)
  rw [Cardinal.mk_fintype, finrank_eq_card_basis h]
Finite Rank Equals Basis Cardinality for Finite-Dimensional Modules (Cardinal Version)
Informal description
Let $M$ be a finite-dimensional module over a ring $R$ with a basis $\{v_i\}_{i \in \iota}$. Then the finite rank of $M$ over $R$, when viewed as a cardinal number, is equal to the cardinality of the index set $\iota$, i.e., $\text{finrank}_R(M) = |\iota|$.
Module.finrank_eq_card_finset_basis theorem
{ι : Type w} {b : Finset ι} (h : Basis b R M) : finrank R M = Finset.card b
Full source 
/-- If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis. This lemma uses a `Finset` instead of indexed types. -/
theorem finrank_eq_card_finset_basis {ι : Type w} {b : Finset ι} (h : Basis b R M) :
    finrank R M = Finset.card b := by rw [finrank_eq_card_basis h, Fintype.card_coe]
Finite Rank Equals Basis Cardinality for Modules with Finite Basis
Informal description
Let $M$ be a module over a ring $R$ with a finite basis $b$ (represented as a finite set of indices). Then the finite rank of $M$ over $R$ is equal to the cardinality of $b$, i.e., $\text{finrank}_R(M) = |b|$.
Module.finrank_self theorem
: finrank R R = 1
Full source 
/-- A ring satisfying `StrongRankCondition` (such as a `DivisionRing`) is one-dimensional as a
module over itself. -/
@[simp]
theorem finrank_self : finrank R R = 1 :=
  finrank_eq_of_rank_eq (by simp)
Finite Rank Identity: $\text{finrank}_R R = 1$
Informal description
For any ring $R$ satisfying the strong rank condition, the finite rank of $R$ as a module over itself is equal to $1$, i.e., $\text{finrank}_R R = 1$.
Basis.unique definition
{ι : Type*} (b : Basis ι R R) : Unique ι
Full source 
/-- Given a basis of a ring over itself indexed by a type `ι`, then `ι` is `Unique`. -/
noncomputable def _root_.Basis.unique {ι : Type*} (b : Basis ι R R) : Unique ι := by
  have : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm
  have : SubsingletonSubsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]
  exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 this)
Uniqueness of Basis Index for a Ring over Itself
Informal description
Given a basis \( b \) of a ring \( R \) over itself indexed by a type \( \iota \), the type \( \iota \) is uniquely determined (i.e., it has exactly one element up to isomorphism). This follows from the fact that the rank of \( R \) as a module over itself is 1, implying that any basis must consist of a single element.
Module.rank_lt_aleph0 theorem
[Module.Finite R M] : Module.rank R M < ℵ₀
Full source 
/-- The rank of a finite module is finite. -/
theorem rank_lt_aleph0 [Module.Finite R M] : Module.rank R M < ℵ₀ := by
  simp only [Module.rank_def]
  obtain ⟨S, hS⟩ := Module.finite_def.mp ‹_›
  refine (ciSup_le' fun i => ?_).trans_lt (nat_lt_aleph0 S.card)
  exact linearIndependent_le_span_finset _ i.prop S hS
Finite Rank of Finite Modules
Informal description
For a finite $R$-module $M$, the rank of $M$ is finite, i.e., $\text{rank}_R M < \aleph_0$.
Module.instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan instance
{R M : Type*} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set M} [Module.Finite R (span R t)] (hs : LinearIndepOn R id s) (hst : s ⊆ t) : Fintype (hs.extend hst)
Full source 
noncomputable instance {R M : Type*} [DivisionRing R] [AddCommGroup M] [Module R M]
    {s t : Set M} [Module.Finite R (span R t)]
    (hs : LinearIndepOn R id s) (hst : s ⊆ t) :
    Fintype (hs.extend hst) := by
  refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)
  rw [← rank_span_set (hs.linearIndepOn_extend hst), hs.span_extend_eq_span]
  exact Module.rank_lt_aleph0 ..
Finiteness of Extended Linearly Independent Sets in Finite-Dimensional Modules
Informal description
For any division ring $R$ and $R$-module $M$, given a linearly independent subset $s$ of $M$ contained in a subset $t$ such that the span of $t$ is finite-dimensional, the extension of $s$ to a maximal linearly independent subset within $t$ is finite.
Module.finrank_eq_rank theorem
[Module.Finite R M] : ↑(finrank R M) = Module.rank R M
Full source 
/-- If `M` is finite, `finrank M = rank M`. -/
@[simp]
theorem finrank_eq_rank [Module.Finite R M] : ↑(finrank R M) = Module.rank R M := by
  rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]
Equality of Finite Rank and Rank for Finite Modules
Informal description
For a finite module $M$ over a ring $R$, the finrank of $M$ (as a natural number) is equal to the rank of $M$ (as a cardinal number), i.e., $\text{finrank}_R M = \text{rank}_R M$.
Submodule.finrank_eq_rank theorem
[Module.Finite R M] (N : Submodule R M) : finrank R N = Module.rank R N
Full source 
/-- If `M` is finite, then `finrank N = rank N` for all `N : Submodule M`. Note that
such an `N` need not be finitely generated. -/
protected theorem _root_.Submodule.finrank_eq_rank [Module.Finite R M] (N : Submodule R M) :
    finrank R N = Module.rank R N := by
  rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]
  exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)
Equality of Finite Rank and Rank for Submodules of Finite Modules
Informal description
For a finite module $M$ over a ring $R$ and any submodule $N$ of $M$, the finite rank of $N$ equals the rank of $N$, i.e., $\text{finrank}_R(N) = \text{rank}_R(N)$.
LinearMap.finrank_le_finrank_of_injective theorem
[Module.Finite R M'] {f : M →ₗ[R] M'} (hf : Function.Injective f) : finrank R M ≤ finrank R M'
Full source 
theorem LinearMap.finrank_le_finrank_of_injective [Module.Finite R M'] {f : M →ₗ[R] M'}
    (hf : Function.Injective f) : finrank R M ≤ finrank R M' :=
  finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_le_of_injective _ hf) (rank_lt_aleph0 _ _)
Finrank Inequality for Injective Linear Maps: $\text{finrank}_R M \leq \text{finrank}_R M'$
Informal description
Let $R$ be a ring and $M$, $M'$ be finite $R$-modules. For any injective linear map $f \colon M \to M'$, the finrank of $M$ is less than or equal to the finrank of $M'$, i.e., $\text{finrank}_R M \leq \text{finrank}_R M'$.
LinearMap.finrank_range_le theorem
[Module.Finite R M] (f : M →ₗ[R] M') : finrank R (LinearMap.range f) ≤ finrank R M
Full source 
theorem LinearMap.finrank_range_le [Module.Finite R M] (f : M →ₗ[R] M') :
    finrank R (LinearMap.range f) ≤ finrank R M :=
  finrank_le_finrank_of_rank_le_rank (lift_rank_range_le f) (rank_lt_aleph0 _ _)
Finrank of Range is Bounded by Finrank of Source Module
Informal description
For a finite $R$-module $M$ and any linear map $f \colon M \to M'$, the finrank (finite dimension) of the range of $f$ is at most the finrank of $M$, i.e., $\text{finrank}_R(\text{range}(f)) \leq \text{finrank}_R(M)$.
LinearMap.finrank_le_of_isSMulRegular theorem
{S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R L'] {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') : Module.finrank R L ≤ Module.finrank R L'
Full source 
theorem LinearMap.finrank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R]
    [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R L'] {s : S}
    (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') :
    Module.finrank R L ≤ Module.finrank R L' := by
  refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_
  rw [← Module.finrank_eq_rank R L']
  exact nat_lt_aleph0 (finrank R ↥L')
Finrank Inequality under Regular Scalar Multiplication: $\text{finrank}_R(L) \leq \text{finrank}_R(L')$
Informal description
Let $R$ be a ring, $S$ a commutative semiring with an algebra structure over $R$, and $M$ a module over both $R$ and $S$ such that the scalar multiplications are compatible via the `IsScalarTower` condition. Let $L$ and $L'$ be submodules of $M$ over $R$, with $L'$ being finite-dimensional over $R$. Let $s \in S$ be an element that is left-regular for the scalar multiplication on $M$ (i.e., $s \cdot x = 0$ implies $x = 0$ for all $x \in M$). If for every $x \in L$, we have $s \cdot x \in L'$, then the finite rank of $L$ is less than or equal to the finite rank of $L'$, i.e., $\text{finrank}_R(L) \leq \text{finrank}_R(L')$.
Submodule.exists_finset_span_eq_linearIndepOn theorem
: ∃ t : Finset M, ↑t ⊆ s ∧ t.card = finrank K (span K s) ∧ span K t = span K s ∧ LinearIndepOn K id (t : Set M)
Full source 
/-- This is a version of `exists_linearIndependent`
with an upper estimate on the size of the finite set we choose. -/
theorem exists_finset_span_eq_linearIndepOn :
    ∃ t : Finset M, ↑t ⊆ s ∧ t.card = finrank K (span K s) ∧
      span K t = span K s ∧ LinearIndepOn K id (t : Set M) := by
  rcases exists_linearIndependent K s with ⟨t, ht_sub, ht_span, ht_indep⟩
  obtain ⟨t, rfl, ht_card⟩ : ∃ u : Finset M, ↑u = t ∧ u.card = finrank K (span K s) := by
    rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
  exact ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
Existence of Finite Spanning Set with Matching Rank and Linear Independence
Informal description
For any subset $s$ of a $K$-module $M$, there exists a finite subset $t \subseteq s$ such that: 1. The cardinality of $t$ equals the finite rank of the submodule spanned by $s$ over $K$, i.e., $|t| = \text{finrank}_K(\text{span}_K(s))$. 2. The submodule spanned by $t$ over $K$ equals the submodule spanned by $s$ over $K$, i.e., $\text{span}_K(t) = \text{span}_K(s)$. 3. The set $t$ is linearly independent over $K$ (with respect to the identity map).
Submodule.exists_fun_fin_finrank_span_eq theorem
: ∃ f : Fin (finrank K (span K s)) → M, (∀ i, f i ∈ s) ∧ span K (range f) = span K s ∧ LinearIndependent K f
Full source 
theorem exists_fun_fin_finrank_span_eq :
    ∃ f : Fin (finrank K (span K s)) → M, (∀ i, f i ∈ s) ∧ span K (range f) = span K s ∧
      LinearIndependent K f := by
  rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, hts, ht_card, ht_span, ht_indep⟩
  set e := (Finset.equivFinOfCardEq ht_card).symm
  exact ⟨(↑) ∘ e, fun i ↦ hts (e i).2, by simpa, ht_indep.comp _ e.injective⟩
Existence of Linearly Independent Spanning Function with Matching Rank
Informal description
For any subset $s$ of a $K$-module $M$, there exists a function $f : \text{Fin}(n) \to M$ where $n = \text{finrank}_K(\text{span}_K(s))$, such that: 1. Each $f(i) \in s$ for all $i \in \text{Fin}(n)$, 2. The submodule spanned by the range of $f$ equals the submodule spanned by $s$, i.e., $\text{span}_K(\text{range}(f)) = \text{span}_K(s)$, 3. The family $\{f(i)\}_{i \in \text{Fin}(n)}$ is linearly independent over $K$.
Submodule.mem_span_set_iff_exists_finsupp_le_finrank theorem
: x ∈ span K s ↔ ∃ c : M →₀ K, c.support.card ≤ finrank K (span K s) ∧ ↑c.support ⊆ s ∧ c.sum (fun mi r ↦ r • mi) = x
Full source 
/-- This is a version of `mem_span_set` with an estimate on the number of terms in the sum. -/
theorem mem_span_set_iff_exists_finsupp_le_finrank :
    x ∈ span K sx ∈ span K s ↔ ∃ c : M →₀ K, c.support.card ≤ finrank K (span K s) ∧
      ↑c.support ⊆ s ∧ c.sum (fun mi r ↦ r • mi) = x := by
  constructor
  · intro h
    rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
    rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩
    refine ⟨c, ?_, hct.trans ht_sub, hx⟩
    exact ht_card ▸ Finset.card_mono hct
  · rintro ⟨c, -, hcs, hx⟩
    exact mem_span_set.mpr ⟨c, hcs, hx⟩
Span Membership via Finite Support with Rank Bound
Informal description
An element $x$ belongs to the span of a subset $s$ of a $K$-module $M$ if and only if there exists a finitely supported function $c : M \to K$ such that: 1. The cardinality of the support of $c$ is at most the finite rank of $\text{span}_K(s)$, 2. The support of $c$ is contained in $s$, and 3. The sum $\sum_{m_i \in \text{supp}(c)} c(m_i) \cdot m_i$ equals $x$.
Algebra.IsQuadraticExtension structure
(R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] extends Module.Free R S
Full source 
/--
An extension of rings `R ⊆ S` is quadratic if `S` is a free `R`-algebra of rank `2`.
-/
-- TODO. use this in connection with `NumberTheory.Zsqrtd`
class IsQuadraticExtension (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S]
    [Algebra R S] extends Module.Free R S where
  finrank_eq_two' : Module.finrank R S = 2
Quadratic Ring Extension
Informal description
An extension of rings \( R \subseteq S \) is called *quadratic* if \( S \) is a free \( R \)-algebra of rank 2. This means that \( S \) is a free \( R \)-module with a basis of size 2, and the multiplication in \( S \) is compatible with the \( R \)-algebra structure.
Algebra.IsQuadraticExtension.finrank_eq_two theorem
(R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] [IsQuadraticExtension R S] : Module.finrank R S = 2
Full source 
theorem IsQuadraticExtension.finrank_eq_two (R S : Type*) [CommSemiring R] [StrongRankCondition R]
    [Semiring S] [Algebra R S] [IsQuadraticExtension R S] :
    Module.finrank R S = 2 := finrank_eq_two'
Rank of Quadratic Extension is Two
Informal description
For a quadratic ring extension \( R \subseteq S \) where \( R \) is a commutative semiring satisfying the strong rank condition and \( S \) is a semiring with an \( R \)-algebra structure, the rank of \( S \) as a free \( R \)-module is equal to 2, i.e., \(\text{finrank}_R S = 2\).