Documentation

Mathlib.Algebra.MonoidAlgebra.Cardinal

Cardinality of monoid algebras #

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

source
📐 coverage
@[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'
source
📐 coverage
@[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'
source
📐 coverage
@[deprecated MonoidAlgebra.cardinalMk_eq_lift_of_fintype (since := "2026-03-26")]
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'

Alias of MonoidAlgebra.cardinalMk_eq_lift_of_fintype.

source
📐 coverage
theorem MonoidAlgebra.cardinalMk_of_fintype (R M : Type u) [Semiring R] [Fintype M] :
Cardinal.mk (MonoidAlgebra R M) = Cardinal.mk R ^ Fintype.card M
source
📐 coverage
theorem AddMonoidAlgebra.cardinalMk_of_fintype (R M : Type u) [Semiring R] [Fintype M] :
Cardinal.mk (AddMonoidAlgebra R M) = Cardinal.mk R ^ Fintype.card M
source
📐 coverage
@[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'))
source
📐 coverage
@[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'))
source
📐 coverage
@[deprecated MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite (since := "2026-03-26")]
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'))

Alias of MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite.

source
📐 coverage
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)
source
📐 coverage
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)
source
📐 coverage
@[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'))
source
📐 coverage
@[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'))
source
📐 coverage
@[deprecated MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite' (since := "2026-03-26")]
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'))

Alias of MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite'.

source
📐 coverage
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)
source
📐 coverage
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)