Drop normalized_eq_self for duplicate normalize_eq

leanprover-community · Nov 17, 2023 · b485a99 · b485a99
1 parent 7b96a04
commit b485a99
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 7 deletions.
diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean
@@ -96,11 +96,6 @@ lemma normalizedFactors_multiset_prod {M} [CancelCommMonoidWithZero M] [UniqueFa
 lemma isUnit_iff_eq_one {M : Type*} [Monoid M] [Unique Mˣ] {x : M} : IsUnit x ↔ x = 1 :=
   ⟨fun h ↦ congr_arg Units.val (Subsingleton.elim (h.unit) 1), fun h ↦ h ▸ isUnit_one⟩
 
--- Mathlib/RingTheory/UniqueFactorizationDomain.lean
-lemma normalized_eq_self {M : Type*} [CancelCommMonoidWithZero M] [Unique Mˣ]
-    [NormalizationMonoid M] {x : M} : normalize x = x := by
-  rw [normalize_apply, Subsingleton.elim (normUnit x) 1, Units.val_one, mul_one]
-
 -- Mathlib/RingTheory/UniqueFactorizationDomain.lean
 lemma factors_pow_count_prod {M} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [DecidableEq M] {x : M}
     (hx : x ≠ 0) : Associated (∏ p in (factors x).toFinset, p ^ (factors x).count p) x := by

diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
@@ -100,10 +100,10 @@ lemma comap_map_eq_of_isUnramified [IsGalois K L] [IsUnramified R S] (I : Ideal
     congr
     rw [dif_pos hp]
     apply PartENat.natCast_inj.mp
-    rw [← normalized_eq_self (x := P), factors_eq_normalizedFactors,
+    rw [← normalize_eq P, factors_eq_normalizedFactors,
       ← multiplicity_eq_count_normalizedFactors
         (prime_of_mem_primesOver hpbot hP).irreducible hIbot,
-      ← normalized_eq_self (x := 𝔓 p hp), ← multiplicity_eq_count_normalizedFactors
+      ← normalize_eq (𝔓 p hp), ← multiplicity_eq_count_normalizedFactors
         (prime_of_mem_primesOver hpbot <| h𝔓' p hp).irreducible hIbot,
       multiplicity.multiplicity_eq_multiplicity_iff]
     intro n