Theorems · Theorem · linear algebra

Ideal.rank_eq

∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [StrongRankCondition R] [inst_2 : Ring S] [IsDomain S]
  [inst_4 : Algebra R S] {n : Type u_4} {m : Type u_5} [inst_5 : Fintype n] [inst_6 : Fintype m]
  (b : Module.Basis n R S) {I : Ideal S}, I ≠ ⊥ → ∀ (c : Module.Basis m R ↥I), Fintype.card m = Fintype.card n

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.

Defined in

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingStrongRankConditionRingIsDomainAlgebraFintypeFintype