bump to nightly-2023-03-21-12

mathlib commit leanprover-community/mathlib@290a7ba
leanprover-community · Mar 21, 2023 · 92a91f2 · 92a91f2
1 parent 6d6cfea
commit 92a91f2
Show file tree

Hide file tree

Showing 5 changed files with 886 additions and 12 deletions.
diff --git a/Mathbin/Algebra/Squarefree.lean b/Mathbin/Algebra/Squarefree.lean
@@ -267,7 +267,7 @@ theorem squarefree_iff_nodup_normalizedFactors [NormalizationMonoid R] [Decidabl
 theorem dvd_pow_iff_dvd_of_squarefree {x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) :
     x ∣ y ^ n ↔ x ∣ y := by
   classical
-    haveI := UniqueFactorizationMonoid.toGcdMonoid R
+    haveI := UniqueFactorizationMonoid.toGCDMonoid R
     exact ⟨hsq.is_radical n y, fun h => h.pow h0⟩
 #align unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree
 

diff --git a/Mathbin/RingTheory/DedekindDomain/Ideal.lean b/Mathbin/RingTheory/DedekindDomain/Ideal.lean
@@ -894,7 +894,7 @@ theorem sup_mul_inf (I J : Ideal A) : (I ⊔ J) * (I ⊓ J) = I * J :=
   by
   letI := Classical.decEq (Ideal A)
   letI := Classical.decEq (Associates (Ideal A))
-  letI := UniqueFactorizationMonoid.toNormalizedGcdMonoid (Ideal A)
+  letI := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
   have hgcd : gcd I J = I ⊔ J :=
     by
     rw [gcd_eq_normalize _ _, normalize_eq]