chore: forward-port leanprover-community/mathlib#18598 (#2928)

leanprover-community · Mar 18, 2023 · 415e0ba · 415e0ba
1 parent 7922ef5
commit 415e0ba
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 13 deletions.
diff --git a/Mathlib/Algebra/CharZero/Lemmas.lean b/Mathlib/Algebra/CharZero/Lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.char_zero.lemmas
-! leanprover-community/mathlib commit 9116dd6709f303dcf781632e15fdef382b0fc579
+! leanprover-community/mathlib commit acee671f47b8e7972a1eb6f4eed74b4b3abce829
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -44,7 +44,7 @@ theorem cast_pow_eq_one {R : Type _} [Semiring R] [CharZero R] (q : ℕ) (n :
 #align nat.cast_pow_eq_one Nat.cast_pow_eq_one
 
 @[simp, norm_cast]
-theorem cast_div_charZero {k : Type _} [Field k] [CharZero k] {m n : ℕ} (n_dvd : n ∣ m) :
+theorem cast_div_charZero {k : Type _} [DivisionSemiring k] [CharZero k] {m n : ℕ} (n_dvd : n ∣ m) :
     ((m / n : ℕ) : k) = m / n := by
   rcases eq_or_ne n 0 with (rfl | hn)
   · simp

diff --git a/Mathlib/Data/Int/Cast/Field.lean b/Mathlib/Data/Int/Cast/Field.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 
 ! This file was ported from Lean 3 source module data.int.cast.field
-! leanprover-community/mathlib commit ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
+! leanprover-community/mathlib commit acee671f47b8e7972a1eb6f4eed74b4b3abce829
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -31,21 +31,21 @@ variable {α : Type _}
 
 /-- Auxiliary lemma for norm_cast to move the cast `-↑n` upwards to `↑-↑n`.
 
-(The restriction to `Field` is necessary, otherwise this would also apply in the case where
+(The restriction to `DivisionRing` is necessary, otherwise this would also apply in the case where
 `R = ℤ` and cause nontermination.)
 -/
 @[norm_cast]
-theorem cast_neg_natCast {R} [Field R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
+theorem cast_neg_natCast {R} [DivisionRing R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp
 #align int.cast_neg_nat_cast Int.cast_neg_natCast
 
 @[simp]
-theorem cast_div [Field α] {m n : ℤ} (n_dvd : n ∣ m) (n_nonzero : (n : α) ≠ 0) :
+theorem cast_div [DivisionRing α] {m n : ℤ} (n_dvd : n ∣ m) (n_nonzero : (n : α) ≠ 0) :
     ((m / n : ℤ) : α) = m / n := by
   rcases n_dvd with ⟨k, rfl⟩
   have : n ≠ 0 := by
     rintro rfl
     simp at n_nonzero
-  rw [Int.mul_ediv_cancel_left _ this, Int.cast_mul, mul_div_cancel_left _ n_nonzero]
+  rw [Int.mul_ediv_cancel_left _ this, mul_comm n k, Int.cast_mul, mul_div_cancel _ n_nonzero]
 #align int.cast_div Int.cast_div
 
 end Int
diff --git a/Mathlib/Data/Int/CharZero.lean b/Mathlib/Data/Int/CharZero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.int.char_zero
-! leanprover-community/mathlib commit ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
+! leanprover-community/mathlib commit acee671f47b8e7972a1eb6f4eed74b4b3abce829
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -47,7 +47,7 @@ theorem cast_ne_zero [AddGroupWithOne α] [CharZero α] {n : ℤ} : (n : α) ≠
 #align int.cast_ne_zero Int.cast_ne_zero
 
 @[simp, norm_cast]
-theorem cast_div_charZero {k : Type _} [Field k] [CharZero k] {m n : ℤ} (n_dvd : n ∣ m) :
+theorem cast_div_charZero {k : Type _} [DivisionRing k] [CharZero k] {m n : ℤ} (n_dvd : n ∣ m) :
     ((m / n : ℤ) : k) = m / n := by
   rcases eq_or_ne n 0 with (rfl | hn)
   · simp [Int.ediv_zero]

diff --git a/Mathlib/Data/Nat/Cast/Field.lean b/Mathlib/Data/Nat/Cast/Field.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yaël Dillies, Patrick Stevens
 
 ! This file was ported from Lean 3 source module data.nat.cast.field
-! leanprover-community/mathlib commit 9116dd6709f303dcf781632e15fdef382b0fc579
+! leanprover-community/mathlib commit acee671f47b8e7972a1eb6f4eed74b4b3abce829
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -29,16 +29,17 @@ namespace Nat
 variable {α : Type _}
 
 @[simp]
-theorem cast_div [Field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n : α) ≠ 0) :
+theorem cast_div [DivisionSemiring α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n : α) ≠ 0) :
     ((m / n : ℕ) : α) = m / n := by
   rcases n_dvd with ⟨k, rfl⟩
   have : n ≠ 0 := by
     rintro rfl
     simp at n_nonzero
-  rw [Nat.mul_div_cancel_left _ this.bot_lt, cast_mul, mul_div_cancel_left _ n_nonzero]
+  rw [Nat.mul_div_cancel_left _ this.bot_lt, mul_comm n k,cast_mul, mul_div_cancel _ n_nonzero]
 #align nat.cast_div Nat.cast_div
 
-theorem cast_div_div_div_cancel_right [Field α] [CharZero α] {m n d : ℕ} (hn : d ∣ n) (hm : d ∣ m) :
+theorem cast_div_div_div_cancel_right [DivisionSemiring α] [CharZero α] {m n d : ℕ}
+  (hn : d ∣ n) (hm : d ∣ m) :
     (↑(m / d) : α) / (↑(n / d) : α) = (m : α) / n := by
   rcases eq_or_ne d 0 with (rfl | hd); · simp [zero_dvd_iff.mp hm]
   replace hd : (d : α) ≠ 0;