mathlib

ed919b61 - feat(algebra/algebraic_card): Cardinality of algebraic numbers (#12869)

feat(algebra/algebraic_card): Cardinality of algebraic numbers (#12869) We prove the following result: the cardinality of algebraic numbers under an R-algebra is at most `# polynomial R * ω`.