R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ (#(p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    (#(i : R[X]) × ↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) i)})
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ (#(p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    sum fun p => #↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p)}
rw [← mk_sigma]
no goals
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ (#(p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    (#(i : R[X]) × ↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) i)})
rfl
no goals
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ max (max (max (#R) ℵ₀) ℵ₀) ℵ₀ = max (#R) ℵ₀
simp only [max_assoc, max_comm ℵ₀, max_left_comm ℵ₀, max_self]