Commit 2024-10-29 15:17 17d5955a

View on Github →

feat: cardinalities of free constructions and Nonempty (CommRing α) (#18364) Zulip thread

Estimated changes

added theorem FreeGroup.norm_of_pow
added theorem FreeGroup.pow_mk
added theorem Cardinal.mk_additive
added theorem Cardinal.mk_freeGroup
added theorem Cardinal.mk_freeMonoid
added theorem Cardinal.mk_freeRing
added theorem nonempty_commRing_iff
added theorem nonempty_ring_iff
added theorem nonempty_semiring_iff