Commit 2024-11-11 08:54 10b85c94

feat: add results on cardinality of localization (#18004)

• OreLocalization.oreDiv_one_surjective_of_finite_(left|right): if S or X is finite, then the natural map X → X[S⁻¹] is surjective
• OreLocalization.numeratorHom_surjective_of_finite: if S is finite, then the natural map R → R[S⁻¹] is surjective
• OreLocalization.cardinalMk_le_max: #X[S⁻¹] ≤ max(#S, #X)
• OreLocalization.cardinalMk_le: #R[S⁻¹] ≤ #R
• OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute: if S is commutative, then #X[S⁻¹] ≤ #X (I don't know how to remove the commutative assumption)
• OreLocalization.cardinalMk: if S has no zero divisors, then #R[S⁻¹] = #R Also the [lift_]cardinalMk_le and [lift_]cardinalMk for Localization, IsLocalization, FractionRing and IsFractionRing. Also change the direction of the conclusion of the existing IsLocalization.card (renamed to IsLocalization.cardinalMk) to match the docstring in file header. It is not directly used in any other files.