R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : (#R) ≤ ℵ₀
hK : ℵ₀ < (#K)
this : ℵ₀ ≤ (#ι)
⊢ (#R) ≤ (#ι)

R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : (#R) ≤ ℵ₀
hK : ℵ₀ < (#K)
this : ℵ₀ ≤ (#ι)
⊢ ℵ₀ ≤ max (#R) (#ι)
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : (#R) ≤ ℵ₀
hK : ℵ₀ < (#K)
this : ℵ₀ ≤ (#ι)
⊢ max (max (#R) (#ι)) ℵ₀ = (#ι)
rw [max_eq_left, max_eq_right]
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✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : (#R) ≤ ℵ₀
hK : ℵ₀ < (#K)
this : ℵ₀ ≤ (#ι)
⊢ (#R) ≤ (#ι)
exact le_trans hR this
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✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : (#R) ≤ ℵ₀
hK : ℵ₀ < (#K)
this : ℵ₀ ≤ (#ι)
⊢ ℵ₀ ≤ max (#R) (#ι)
exact le_max_of_le_right this