Theorems · Theorem · field theory

IsTranscendenceBasis.lift_rank_eq_max_lift

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type w} {x : ι → E}
  [Nonempty ι],
  IsTranscendenceBasis F x →
    Cardinal.lift.{max u w, v} (Module.rank F 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: Field Field Algebra Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites43

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

Moduleproof · cited by 20,661
AddCommGroupproof · cited by 12,871
Algebrastatement and proof · cited by 11,388
Ringproof · cited by 7,463
Fieldstatement and proof · cited by 7,404
Set.rangeproof · cited by 4,705
LE.le.transproof · cited by 3,151
Cardinalstatement and proof · cited by 2,598
Nontrivialproof · cited by 2,416
IsDomainproof · cited by 2,196
MvPolynomialproof · cited by 2,140
LT.lt.ne'proof · cited by 1,417

Cited by1

Results whose statement or proof uses this declaration.

Algebra.Transcendental.rank_eq_cardinalMkproof · cited by 1