R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift (#{ x // IsAlgebraic R x }) ≤ max (lift (#R)) ℵ₀
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ (#{ x // IsAlgebraic R x }) ≤ max (#R) ℵ₀
rw [← lift_id (#_), ← lift_id (#R)]
no goals
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift (#{ x // IsAlgebraic R x }) ≤ max (lift (#R)) ℵ₀
exact cardinal_mk_lift_le_max R A