# mathlibdocumentation

ring_theory.localization.cardinality

# 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 is_localization.unique_of_zero_mem).

## Main statements #

• is_localization.card_le: A localization has cardinality no larger than the base ring.
• is_localization.card: If you don't localize at zero-divisors, the localization of a ring has cardinality equal to its base ring,
theorem is_localization.algebra_map_surjective_of_fintype {R : Type u} [comm_ring R] (S : submonoid R) {L : Type u} [comm_ring L] [ L] [ L] [fintype R] :

Localizing a finite ring can only reduce the amount of elements.

theorem is_localization.card_le {R : Type u} [comm_ring R] (S : submonoid R) {L : Type u} [comm_ring L] [ L] [ L] :

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

theorem is_localization.card {R : Type u} [comm_ring R] (S : submonoid R) (L : Type u) [comm_ring L] [ L] [ L] (hS : S ) :

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