Cardinality of monoid algebras

This file computes the cardinality of R[M] in terms of #R and #M.

@[simp]

theorem MonoidAlgebra.cardinalMk_lift_of_fintype (R : Type u) (M' : Type v) [Semiring R] [Fintype M'] : Cardinal.mk (MonoidAlgebra R M') = Cardinal.lift.{v, u} (Cardinal.mk R) ^ Fintype.card M'

@[simp]

theorem AddMonoidAlgebra.cardinalMk_lift_of_fintype (R : Type u) (M' : Type v) [Semiring R] [Fintype M'] : Cardinal.mk (AddMonoidAlgebra R M') = Cardinal.lift.{v, u} (Cardinal.mk R) ^ Fintype.card M'

theorem MonoidAlgebra.cardinalMk_of_fintype (R M : Type u) [Semiring R] [Fintype M] : Cardinal.mk (MonoidAlgebra R M) = Cardinal.mk R ^ Fintype.card M

theorem AddMonoidAlgebra.cardinalMk_of_fintype (R M : Type u) [Semiring R] [Fintype M] : Cardinal.mk (AddMonoidAlgebra R M) = Cardinal.mk R ^ Fintype.card M

@[simp]

theorem MonoidAlgebra.cardinalMk_lift_of_infinite (R : Type u) (M' : Type v) [Semiring R] [Infinite M'] [Nontrivial R] : Cardinal.mk (MonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))

@[simp]

theorem AddMonoidAlgebra.cardinalMk_lift_of_infinite (R : Type u) (M' : Type v) [Semiring R] [Infinite M'] [Nontrivial R] : Cardinal.mk (AddMonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))

theorem MonoidAlgebra.cardinalMk_of_infinite (R M : Type u) [Semiring R] [Infinite M] [Nontrivial R] : Cardinal.mk (MonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)

theorem AddMonoidAlgebra.cardinalMk_of_infinite (R M : Type u) [Semiring R] [Infinite M] [Nontrivial R] : Cardinal.mk (AddMonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)

@[simp]

theorem MonoidAlgebra.cardinalMk_lift_of_infinite' (R : Type u) (M' : Type v) [Semiring R] [Nonempty M'] [Infinite R] : Cardinal.mk (MonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))

@[simp]

theorem AddMonoidAlgebra.cardinalMk_lift_of_infinite' (R : Type u) (M' : Type v) [Semiring R] [Nonempty M'] [Infinite R] : Cardinal.mk (AddMonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))

theorem MonoidAlgebra.cardinalMk_of_infinite' (R M : Type u) [Semiring R] [Nonempty M] [Infinite R] : Cardinal.mk (MonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)

theorem AddMonoidAlgebra.cardinalMk_of_infinite' (R M : Type u) [Semiring R] [Nonempty M] [Infinite R] : Cardinal.mk (AddMonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)