IsLocalization.card_le
theorem IsLocalization.card_le :
∀ {R : Type u} [inst : CommRing R] (S : Submonoid R) {L : Type u} [inst_1 : CommRing L] [inst_2 : Algebra R L]
[inst : IsLocalization S L], Cardinal.mk L ≤ Cardinal.mk R
This theorem states that for any type `R` that forms a commutative ring, given a submonoid `S` of `R` and another type `L` that also forms a commutative ring and is an algebra over `R`, if `L` is a localization of `R` with respect to `S`, then the cardinality of `L` is always less than or equal to the cardinality of `R`. In simpler terms, a localization cannot have more elements than the base ring it is derived from.
More concisely: For any commutative rings `R`, submonoid `S` of `R`, and commutative `R`-algebra `L` that is a localization of `R` with respect to `S`, the cardinality of `L` is less than or equal to the cardinality of `R`.
|
IsLocalization.card
theorem IsLocalization.card :
∀ {R : Type u} [inst : CommRing R] (S : Submonoid R) (L : Type u) [inst_1 : CommRing L] [inst_2 : Algebra R L]
[inst_3 : IsLocalization S L], S ≤ nonZeroDivisors R → Cardinal.mk R = Cardinal.mk L
The theorem `IsLocalization.card` states that for any commutative ring `R`, a submonoid `S` of `R`, and another commutative ring `L` that is a localization of `R` at `S`, if `S` is a subset of the submonoid of non-zero-divisors of `R`, then the cardinality of `R` is the same as the cardinality of `L`. In other words, if you do not localize at any zero-divisors, localization of a commutative ring preserves its cardinality.
More concisely: If `R` is a commutative ring, `S` is a submonoid of non-zero-divisors in `R`, and `L` is a localization of `R` at `S`, then the cardinality of `R` equals the cardinality of `L`.
|