Cardinality of monoid algebras

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

@[simp]

theorem MonoidAlgebra.cardinalMk_eq_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_eq_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_eq_max_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_eq_max_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_eq_max_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_eq_max_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)

instance MonoidAlgebra.instInfiniteOfNonempty (R : Type u) (M' : Type v) [Semiring R] [Infinite R] [Nonempty M'] : Infinite (MonoidAlgebra R M')

instance AddMonoidAlgebra.instInfiniteOfNonempty (R : Type u) (M' : Type v) [Semiring R] [Infinite R] [Nonempty M'] : Infinite (AddMonoidAlgebra R M')

instance MonoidAlgebra.instInfiniteOfNontrivial (R : Type u) (M' : Type v) [Semiring R] [Nontrivial R] [Infinite M'] : Infinite (MonoidAlgebra R M')

instance AddMonoidAlgebra.instInfiniteOfNontrivial (R : Type u) (M' : Type v) [Semiring R] [Nontrivial R] [Infinite M'] : Infinite (AddMonoidAlgebra R M')

instance MonoidAlgebra.instCountable (R : Type u) (M' : Type v) [Semiring R] [Countable R] [Countable M'] : Countable (MonoidAlgebra R M')

instance AddMonoidAlgebra.instCountable (R : Type u) (M' : Type v) [Semiring R] [Countable R] [Countable M'] : Countable (AddMonoidAlgebra R M')

instance MonoidAlgebra.instSmall (R : Type u) (M' : Type v) [Semiring R] [Small.{w, u} R] [Small.{w, v} M'] : Small.{w, max v u} (MonoidAlgebra R M')

instance AddMonoidAlgebra.instSmall (R : Type u) (M' : Type v) [Semiring R] [Small.{w, u} R] [Small.{w, v} M'] : Small.{w, max v u} (AddMonoidAlgebra R M')