# Cardinality of localizations #

In this file, we establish the cardinality of localizations. In most cases, a localization has
cardinality equal to the base ring. If there are zero-divisors, however, this is no longer true -
for example, `ZMod 6`

localized at `{2, 4}`

is equal to `ZMod 3`

, and if you have zero in your
submonoid, then your localization is trivial (see `IsLocalization.uniqueOfZeroMem`

).

## Main statements #

`IsLocalization.card_le`

: A localization has cardinality no larger than the base ring.`IsLocalization.card`

: If you don't localize at zero-divisors, the localization of a ring has cardinality equal to its base ring,

theorem
IsLocalization.card_le
{R : Type u}
[CommRing R]
(S : Submonoid R)
{L : Type u}
[CommRing L]
[Algebra R L]
[IsLocalization S L]
:

Cardinal.mk L ≤ Cardinal.mk R

A localization always has cardinality less than or equal to the base ring.

theorem
IsLocalization.card
{R : Type u}
[CommRing R]
(S : Submonoid R)
(L : Type u)
[CommRing L]
[Algebra R L]
[IsLocalization S L]
(hS : S ≤ nonZeroDivisors R)
:

Cardinal.mk R = Cardinal.mk L

If you do not localize at any zero-divisors, localization preserves cardinality.