Cardinality of algebraic numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file, we prove variants of the following result: the cardinality of algebraic numbers under
an R-algebra is at most
# R[X] * ℵ₀.
Although this can be used to prove that real or complex transcendental numbers exist, a more direct
proof is given by