R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ max (#R) (lift (#ℕ)) = max (#R) ℵ₀
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (#AddMonoidAlgebra R ℕ) = max (#R) ℵ₀
rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
no goals
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ max (#R) (lift (#ℕ)) = max (#R) ℵ₀
rfl