no goals
R L K : Type u
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ hv : IsTranscendenceBasis R v
⊢ max (#{ x // x ∈ Algebra.adjoin R (Set.range v) }) ℵ₀ = max (#MvPolynomial ι R) ℵ₀
rw [Cardinal.eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩]
no goals
R L K : Type u
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ hv : IsTranscendenceBasis R v
⊢ max (max (max (#R) (#ι)) ℵ₀) ℵ₀ = max (max (#R) (#ι)) ℵ₀
simp [max_assoc]