Theorems · Theorem · field theory

IsTranscendenceBasis.lift_cardinalMk_eq

∀ {ι : Type u} {ι' : Type u'} {R : Type u_1} {A : Type w} {x : ι → A} {y : ι' → A} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R] [NoZeroDivisors A],
  IsTranscendenceBasis R x →
    IsTranscendenceBasis R y → Cardinal.lift.{u', u} (Cardinal.mk ι) = Cardinal.lift.{u, u'} (Cardinal.mk ι')

Any two transcendence bases of a domain A have the same cardinality. May fail if A is not a domain; see https://mathoverflow.net/a/144580.

Defined in

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraNontrivialNoZeroDivisors