Theorems · Theorem · field theory

Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial

∀ (R : Type u) [inst : CommRing R] [IsDomain R] (L : Type v) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra R L] [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L],
  Cardinal.lift.{u, v} (Cardinal.mk L) ≤ Cardinal.mk ((p : Polynomial R) × { x // x ∈ p.aroots L })

Defined in

Mathlib.RingTheory.Algebraic.Cardinality

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainAlgebraModule.IsTorsionFreeAlgebra.IsAlgebraic