Theorems · Theorem · field theory

IsTranscendenceBasis.lift_cardinalMk_eq_max_lift

∀ {F : Type u} {E : Type v} [inst : CommRing F] [Nontrivial F] [inst_2 : CommRing E] [IsDomain E] [inst_4 : Algebra F E]
  {ι : Type w} {x : ι → E} [Nonempty ι],
  IsTranscendenceBasis F x →
    Cardinal.lift.{max u w, v} (Cardinal.mk E) =
      max (max (Cardinal.lift.{max v w, u} (Cardinal.mk F)) (Cardinal.lift.{max u v, w} (Cardinal.mk ι)))
        Cardinal.aleph0

Defined in: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Cited by: 1 results in Mathlib
Foundations: Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Nontrivial CommRing IsDomain Algebra Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites29

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Set.rangeproof · cited by 4,705
Cardinalstatement · cited by 2,598
Nontrivialstatement and proof · cited by 2,416
IsDomainstatement and proof · cited by 2,196
le_antisymmproof · cited by 2,068
Subalgebraproof · cited by 1,353
Cardinal.mkstatement and proof · cited by 942
Cardinal.liftstatement and proof · cited by 583
Algebra.adjoinproof · cited by 535
Cardinal.aleph0statement and proof · cited by 521

Cited by1

Results whose statement or proof uses this declaration.

Algebra.Transcendental.rank_eq_cardinalMkproof · cited by 1