Cardinalities of free constructions

This file shows that all the free constructions over α have cardinality max #α ℵ₀, and are thus infinite.

Combined with the ring Fin n for the finite cases, this lets us show that there is a CommRing of any cardinality.

instance instInfiniteFreeMonoidOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeMonoid α)

instance instInfiniteFreeAddMonoidOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeAddMonoid α)

instance instInfiniteFreeGroupOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeGroup α)

instance instInfiniteFreeAddGroupOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeAddGroup α)

instance instInfiniteFreeAbelianGroupOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeAbelianGroup α)

instance instInfiniteFreeRing (α : Type u) : Infinite (FreeRing α)

instance instInfiniteFreeCommRing (α : Type u) : Infinite (FreeCommRing α)

theorem Cardinal.mk_abelianization_le (G : Type u) [Group G] : Cardinal.mk (Abelianization G) ≤ Cardinal.mk G

@[simp]

theorem Cardinal.mk_freeMonoid (α : Type u) [Nonempty α] : Cardinal.mk (FreeMonoid α) = Cardinal.mk α ⊔ Cardinal.aleph0

@[simp]

theorem Cardinal.mk_freeAddMonoid (α : Type u) [Nonempty α] : Cardinal.mk (FreeAddMonoid α) = Cardinal.mk α ⊔ Cardinal.aleph0

@[simp]

theorem Cardinal.mk_freeGroup (α : Type u) [Nonempty α] : Cardinal.mk (FreeGroup α) = Cardinal.mk α ⊔ Cardinal.aleph0

@[simp]

theorem Cardinal.mk_freeAddGroup (α : Type u) [Nonempty α] : Cardinal.mk (FreeAddGroup α) = Cardinal.mk α ⊔ Cardinal.aleph0

@[simp]

theorem Cardinal.mk_freeAbelianGroup (α : Type u) [Nonempty α] : Cardinal.mk (FreeAbelianGroup α) = Cardinal.mk α ⊔ Cardinal.aleph0

@[simp]

theorem Cardinal.mk_freeRing (α : Type u) : Cardinal.mk (FreeRing α) = Cardinal.mk α ⊔ Cardinal.aleph0

@[simp]

theorem Cardinal.mk_freeCommRing (α : Type u) : Cardinal.mk (FreeCommRing α) = Cardinal.mk α ⊔ Cardinal.aleph0

instance nonempty_commRing (α : Type u) [Nonempty α] : Nonempty (CommRing α)

A commutative ring can be constructed on any non-empty type.

See also Infinite.nonempty_field.

@[simp]

theorem nonempty_commRing_iff (α : Type u) : Nonempty (CommRing α) ↔ Nonempty α

@[simp]

theorem nonempty_ring_iff (α : Type u) : Nonempty (Ring α) ↔ Nonempty α

@[simp]

theorem nonempty_commSemiring_iff (α : Type u) : Nonempty (CommSemiring α) ↔ Nonempty α

@[simp]

theorem nonempty_semiring_iff (α : Type u) : Nonempty (Semiring α) ↔ Nonempty α