feat(RingTheory/Localization/Integer): cardinality of finsetIntegerMultiple (leanprover-community#41688)

This PR proves injectivity of `integerMultiple` and computes the cardinality of `card_finsetIntegerMultiple`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/RingTheory/Localization/Integer.lean

@@ -124,6 +124,13 @@ theorem map_integerMultiple {ι : Type*} (s : Finset ι) (f : ι → S) (i : s)
     algebraMap R S (integerMultiple M s f i) = commonDenom M s f • f i :=
   ((exist_integer_multiples M s f).choose_spec _ i.prop).choose_spec
 
+theorem integerMultipleMultiple_injective {ι : Type*} (s : Finset ι) (f : ι → S)
+    (hf : Function.Injective f) : Function.Injective (integerMultiple M s f) := by
+  intro i j h
+  rw [← SetLike.coe_eq_coe, ← hf.eq_iff,
+    ← (IsLocalization.smul_bijective S (commonDenom M s f)).injective.eq_iff,
+    ← map_integerMultiple M s f i, ← map_integerMultiple M s f j, h]
+
 /-- A choice of a common multiple of the denominators of a finite set of fractions. -/
 noncomputable def commonDenomOfFinset (s : Finset S) : M :=
   commonDenom M s id
@@ -146,4 +153,10 @@ theorem finsetIntegerMultiple_image [DecidableEq R] (s : Finset S) :
   · rintro ⟨x, hx, rfl⟩
     exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩
 
+@[simp]
+theorem card_finsetIntegerMultiple [DecidableEq R] (s : Finset S) :
+    (finsetIntegerMultiple M s).card = s.card :=
+  (Finset.card_image_of_injective _ (integerMultipleMultiple_injective M s id injective_id)).trans
+    Finset.card_attach
+
 end IsLocalization