Algebraic.cardinal_mk_lift_le_max

theorem Algebraic.cardinal_mk_lift_le_max : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDomain A] [inst_3 : Algebra R A] [inst_4 : NoZeroSMulDivisors R A], Cardinal.lift.{u, v} (Cardinal.mk { x // IsAlgebraic R x }) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk R)) Cardinal.aleph0

This theorem states that for any types `R` and `A` where `R` is a commutative ring, `A` is a commutative ring and a domain, `A` is an `R`-algebra, and `R` and `A` have no zero divisors under scalar multiplication, the cardinality of the set of algebraic elements of `A` over `R` (lifted to a higher universe level if necessary), is less than or equal to the maximum of the cardinality of `R` (lifted to a higher universe level if necessary) and the cardinality of the natural numbers, denoted by `ℵ₀`. In mathematical terms, we can say that the number of algebraic elements in an R-algebra `A` is bounded above by the max of the number of elements in `R` and the cardinality of the set of natural numbers.

More concisely: The number of algebraic elements in a commutative `R`-algebra `A`, where `R` is a commutative ring with no zero divisors and `A` is a commutative domain, is bounded above by the maximum of the cardinalities of `R` and the natural numbers.