bump to nightly-2023-03-18-20

mathlib commit leanprover-community/mathlib@02ba894

Mathbin/Data/Zmod/Quotient.lean

@@ -47,7 +47,7 @@ namespace Int
 /-- `ℤ` modulo multiples of `n : ℕ` is `zmod n`. -/
 def quotientZmultiplesNatEquivZmod : ℤ ⧸ AddSubgroup.zmultiples (n : ℤ) ≃+ ZMod n :=
   (quotientAddEquivOfEq (ZMod.ker_int_castAddHom _)).symm.trans <|
-    quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) coe int_cast_zMod_cast
+    quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) coe int_cast_zmod_cast
 #align int.quotient_zmultiples_nat_equiv_zmod Int.quotientZmultiplesNatEquivZmod
 
 /-- `ℤ` modulo multiples of `a : ℤ` is `zmod a.nat_abs`. -/
@@ -59,7 +59,7 @@ def quotientZmultiplesEquivZmod (a : ℤ) : ℤ ⧸ AddSubgroup.zmultiples a ≃
 def quotientSpanNatEquivZmod : ℤ ⧸ Ideal.span {↑n} ≃+* ZMod n :=
   (Ideal.quotEquivOfEq (ZMod.ker_int_castRingHom _)).symm.trans <|
     RingHom.quotientKerEquivOfRightInverse <|
-      show Function.RightInverse coe (Int.castRingHom (ZMod n)) from int_cast_zMod_cast
+      show Function.RightInverse coe (Int.castRingHom (ZMod n)) from int_cast_zmod_cast
 #align int.quotient_span_nat_equiv_zmod Int.quotientSpanNatEquivZmod
 
 /-- `ℤ` modulo the ideal generated by `a : ℤ` is `zmod a.nat_abs`. -/

Mathbin/FieldTheory/Finite/Basic.lean

@@ -510,7 +510,7 @@ theorem Int.ModEq.pow_card_sub_one_eq_one {p : ℕ} (hp : Nat.Prime p) {n : ℤ}
     rw [CharP.int_cast_eq_zero_iff _ p, ← (nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
     · exact hpn.symm
     exact ZMod.charP p
-  simpa [← ZMod.int_coe_eq_int_coe_iff] using ZMod.pow_card_sub_one_eq_one this
+  simpa [← ZMod.int_cast_eq_int_cast_iff] using ZMod.pow_card_sub_one_eq_one this
 #align int.modeq.pow_card_sub_one_eq_one Int.ModEq.pow_card_sub_one_eq_one
 
 section

Mathbin/GroupTheory/FiniteAbelian.lean

@@ -89,7 +89,7 @@ theorem equiv_directSum_zMod_of_fintype [Finite G] :
 #align add_comm_group.equiv_direct_sum_zmod_of_fintype AddCommGroup.equiv_directSum_zMod_of_fintype
 
 theorem finite_of_fg_torsion [hG' : AddGroup.Fg G] (hG : AddMonoid.IsTorsion G) : Finite G :=
-  @Module.finite_of_fg_torsion _ _ _ (Module.Finite.iff_add_group_fg.mpr hG') <|
+  @Module.finite_of_fg_torsion _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG') <|
     AddMonoid.isTorsion_iff_isTorsion_int.mp hG
 #align add_comm_group.finite_of_fg_torsion AddCommGroup.finite_of_fg_torsion
 

Mathbin/GroupTheory/SpecificGroups/Dihedral.lean

@@ -195,7 +195,7 @@ theorem orderOf_r_one : orderOf (r 1 : DihedralGroup n) = n :=
 -/
 theorem orderOf_r [NeZero n] (i : ZMod n) : orderOf (r i) = n / Nat.gcd n i.val :=
   by
-  conv_lhs => rw [← ZMod.nat_cast_zMod_val i]
+  conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
   rw [← r_one_pow, orderOf_pow, order_of_r_one]
 #align dihedral_group.order_of_r DihedralGroup.orderOf_r
 

Mathbin/GroupTheory/SpecificGroups/Quaternion.lean

@@ -279,7 +279,7 @@ theorem orderOf_a_one : orderOf (a 1 : QuaternionGroup n) = 2 * n :=
 -/
 theorem orderOf_a [NeZero n] (i : ZMod (2 * n)) : orderOf (a i) = 2 * n / Nat.gcd (2 * n) i.val :=
   by
-  conv_lhs => rw [← ZMod.nat_cast_zMod_val i]
+  conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
   rw [← a_one_pow, orderOf_pow, order_of_a_one]
 #align quaternion_group.order_of_a QuaternionGroup.orderOf_a
 

Mathbin/LinearAlgebra/CliffordAlgebra/Grading.lean

@@ -170,7 +170,7 @@ of vectors. -/
 theorem evenOddInduction (n : ZMod 2) {P : ∀ x, x ∈ evenOdd Q n → Prop}
     (hr :
       ∀ (v) (h : v ∈ (ι Q).range ^ n.val),
-        P v (Submodule.mem_supᵢ_of_mem ⟨n.val, n.nat_cast_zMod_val⟩ h))
+        P v (Submodule.mem_supᵢ_of_mem ⟨n.val, n.nat_cast_zmod_val⟩ h))
     (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (Submodule.add_mem _ hx hy))
     (hιι_mul :
       ∀ (m₁ m₂) {x hx},
@@ -181,7 +181,7 @@ theorem evenOddInduction (n : ZMod 2) {P : ∀ x, x ∈ evenOdd Q n → Prop}
   by
   apply Submodule.supᵢ_induction' _ _ (hr 0 (Submodule.zero_mem _)) @hadd
   refine' Subtype.rec _
-  simp_rw [Subtype.coe_mk, ZMod.nat_coe_zMod_eq_iff, add_comm n.val]
+  simp_rw [Subtype.coe_mk, ZMod.nat_coe_zmod_eq_iff, add_comm n.val]
   rintro n' ⟨k, rfl⟩ xv
   simp_rw [pow_add, pow_mul]
   refine' Submodule.mul_induction_on' _ _

Mathbin/NumberTheory/LegendreSymbol/AddCharacter.lean

@@ -302,7 +302,7 @@ theorem zMod_char_isNontrivial_iff (n : ℕ+) (ψ : AddChar (ZMod n) C) : IsNont
   rintro h₁ ⟨a, ha⟩
   have ha₁ : a = a.val • 1 := by
     rw [nsmul_eq_mul, mul_one]
-    exact (ZMod.nat_cast_zMod_val a).symm
+    exact (ZMod.nat_cast_zmod_val a).symm
   rw [ha₁, map_nsmul_pow, h₁, one_pow] at ha
   exact ha rfl
 #align add_char.zmod_char_is_nontrivial_iff AddChar.zMod_char_isNontrivial_iff

Mathbin/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean

@@ -230,7 +230,7 @@ theorem eq_neg_one_iff' {a : ℕ} : legendreSym p a = -1 ↔ ¬IsSquare (a : ZMo
 /-- The number of square roots of `a` modulo `p` is determined by the Legendre symbol. -/
 theorem card_sqrts (hp : p ≠ 2) (a : ℤ) :
     ↑{ x : ZMod p | x ^ 2 = a }.toFinset.card = legendreSym p a + 1 :=
-  quadraticChar_card_sqrts ((ringChar_zMod_n p).substr hp) a
+  quadraticChar_card_sqrts ((ringChar_zmod_n p).substr hp) a
 #align legendre_sym.card_sqrts legendreSym.card_sqrts
 
 end legendreSym

Mathbin/NumberTheory/LucasLehmer.lean

@@ -163,7 +163,7 @@ theorem residue_eq_zero_iff_sMod_eq_zero (p : ℕ) (w : 1 < p) :
   · -- We want to use that fact that `0 ≤ s_mod p (p-2) < 2^p - 1`
     -- and `lucas_lehmer_residue p = 0 → 2^p - 1 ∣ s_mod p (p-2)`.
     intro h
-    simp [ZMod.int_coe_zMod_eq_zero_iff_dvd] at h
+    simp [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h
     apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h <;> clear h
     apply s_mod_nonneg _ (Nat.lt_of_succ_lt w)
     exact s_mod_lt _ (Nat.lt_of_succ_lt w) (p - 2)
@@ -450,7 +450,7 @@ theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
   by
   dsimp [lucas_lehmer_residue] at h
   rw [s_zmod_eq_s p'] at h
-  simp [ZMod.int_coe_zMod_eq_zero_iff_dvd] at h
+  simp [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h
   cases' h with k h
   use k
   replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h
@@ -471,7 +471,7 @@ theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
 /-- `q` is the minimum factor of `mersenne p`, so `M p = 0` in `X q`. -/
 theorem mersenne_coe_x (p : ℕ) : (mersenne p : X (q p)) = 0 :=
   by
-  ext <;> simp [mersenne, q, ZMod.nat_coe_zMod_eq_zero_iff_dvd, -pow_pos]
+  ext <;> simp [mersenne, q, ZMod.nat_cast_zmod_eq_zero_iff_dvd, -pow_pos]
   apply Nat.minFac_dvd
 #align lucas_lehmer.mersenne_coe_X LucasLehmer.mersenne_coe_x
 

Mathbin/NumberTheory/Multiplicity.lean

@@ -285,7 +285,7 @@ theorem Int.sq_mod_four_eq_one_of_odd {x : ℤ} : Odd x → x ^ 2 % 4 = 1 :=
     x ^ 2 % (4 : ℕ) = 1 % (4 : ℕ) := _
     _ = 1 := by norm_num
 
-  rw [← ZMod.int_coe_eq_int_coe_iff'] at hx⊢
+  rw [← ZMod.int_cast_eq_int_cast_iff'] at hx⊢
   push_cast
   rw [← map_intCast (ZMod.castHom (show 2 ∣ 4 by norm_num) (ZMod 2)) x] at hx
   set y : ZMod 4 := x

Mathbin/NumberTheory/Padics/RingHoms.lean

@@ -119,7 +119,7 @@ theorem isUnit_den (r : ℚ) (h : ‖(r : ℚ_[p])‖ ≤ 1) : IsUnit (r.den : 
 theorem norm_sub_mod_part_aux (r : ℚ) (h : ‖(r : ℚ_[p])‖ ≤ 1) :
     ↑p ∣ r.num - r.num * r.den.gcdA p % p * ↑r.den :=
   by
-  rw [← ZMod.int_coe_zMod_eq_zero_iff_dvd]
+  rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
   simp only [Int.cast_ofNat, ZMod.nat_cast_mod, Int.cast_mul, Int.cast_sub]
   have := congr_arg (coe : ℤ → ZMod p) (gcd_eq_gcd_ab r.denom p)
   simp only [Int.cast_ofNat, add_zero, Int.cast_add, ZMod.nat_cast_self, Int.cast_mul,
@@ -162,7 +162,7 @@ theorem zMod_congr_of_sub_mem_span_aux (n : ℕ) (x : ℤ_[p]) (a b : ℤ)
     (hb : x - b ∈ (Ideal.span {p ^ n} : Ideal ℤ_[p])) : (a : ZMod (p ^ n)) = b :=
   by
   rw [Ideal.mem_span_singleton] at ha hb
-  rw [← sub_eq_zero, ← Int.cast_sub, ZMod.int_coe_zMod_eq_zero_iff_dvd, Int.coe_nat_pow]
+  rw [← sub_eq_zero, ← Int.cast_sub, ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.coe_nat_pow]
   rw [← dvd_neg, neg_sub] at ha
   have := dvd_add ha hb
   rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ←
@@ -437,7 +437,7 @@ theorem ker_toZmodPow (n : ℕ) : (toZmodPow n : ℤ_[p] →+* ZMod (p ^ n)).ker
       convert appr_spec n x
       simp only [this, sub_zero, cast_zero]
     dsimp [to_zmod_pow, to_zmod_hom] at h
-    rw [ZMod.nat_coe_zMod_eq_zero_iff_dvd] at h
+    rw [ZMod.nat_cast_zmod_eq_zero_iff_dvd] at h
     apply eq_zero_of_dvd_of_lt h (appr_lt _ _)
   · intro h
     rw [← sub_zero x] at h
@@ -532,7 +532,7 @@ include f_compat
 theorem pow_dvd_nthHom_sub (r : R) (i j : ℕ) (h : i ≤ j) : ↑p ^ i ∣ nthHom f r j - nthHom f r i :=
   by
   specialize f_compat i j h
-  rw [← Int.coe_nat_pow, ← ZMod.int_coe_zMod_eq_zero_iff_dvd, Int.cast_sub]
+  rw [← Int.coe_nat_pow, ← ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.cast_sub]
   dsimp [nth_hom]
   rw [← f_compat, RingHom.comp_apply]
   simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.nat_cast_val, ZMod.int_cast_cast]
@@ -580,7 +580,7 @@ theorem nthHomSeq_add (r s : R) :
   dsimp [nth_hom_seq]
   apply lt_of_le_of_lt _ hn
   rw [← Int.cast_add, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
-    ZMod.int_coe_zMod_eq_zero_iff_dvd]
+    ZMod.int_cast_zmod_eq_zero_iff_dvd]
   dsimp [nth_hom]
   simp only [ZMod.nat_cast_val, RingHom.map_add, Int.cast_sub, ZMod.int_cast_cast, Int.cast_add]
   rw [ZMod.cast_add (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]
@@ -597,7 +597,7 @@ theorem nthHomSeq_mul (r s : R) :
   dsimp [nth_hom_seq]
   apply lt_of_le_of_lt _ hn
   rw [← Int.cast_mul, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
-    ZMod.int_coe_zMod_eq_zero_iff_dvd]
+    ZMod.int_cast_zmod_eq_zero_iff_dvd]
   dsimp [nth_hom]
   simp only [ZMod.nat_cast_val, RingHom.map_mul, Int.cast_sub, ZMod.int_cast_cast, Int.cast_mul]
   rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]
@@ -680,7 +680,7 @@ See also `padic_int.lift_unique`.
 theorem lift_spec (n : ℕ) : (toZmodPow n).comp (lift f_compat) = f n :=
   by
   ext r
-  rw [RingHom.comp_apply, ← ZMod.nat_cast_zMod_val (f n r), ← map_natCast <| to_zmod_pow n, ←
+  rw [RingHom.comp_apply, ← ZMod.nat_cast_zmod_val (f n r), ← map_natCast <| to_zmod_pow n, ←
     sub_eq_zero, ← RingHom.map_sub, ← RingHom.mem_ker, ker_to_zmod_pow]
   apply lift_sub_val_mem_span
 #align padic_int.lift_spec PadicInt.lift_spec

Mathbin/NumberTheory/Pell.lean

@@ -100,14 +100,14 @@ theorem exists_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
     prod.ext_iff.mp hqf
   have hd₁ : m ∣ q₁.1 * q₂.1 - d * (q₁.2 * q₂.2) :=
     by
-    rw [← Int.natAbs_dvd, ← ZMod.int_coe_zMod_eq_zero_iff_dvd]
+    rw [← Int.natAbs_dvd, ← ZMod.int_cast_zmod_eq_zero_iff_dvd]
     push_cast
     rw [hq1, hq2, ← sq, ← sq]
     norm_cast
-    rw [ZMod.int_coe_zMod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
+    rw [ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
   have hd₂ : m ∣ q₁.1 * q₂.2 - q₂.1 * q₁.2 :=
     by
-    rw [← Int.natAbs_dvd, ← ZMod.int_coe_eq_int_coe_iff_dvd_sub]
+    rw [← Int.natAbs_dvd, ← ZMod.int_cast_eq_int_cast_iff_dvd_sub]
     push_cast
     rw [hq1, hq2]
   replace hm₀ : (m : ℚ) ≠ 0 := int.cast_ne_zero.mpr hm₀

Mathbin/NumberTheory/PrimesCongruentOne.lean

@@ -48,7 +48,7 @@ theorem exists_prime_gt_modEq_one {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) :
   have hroot : is_root (cyclotomic k (ZMod p)) (cast_ring_hom (ZMod p) b) :=
     by
     rw [is_root.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_cast_ring_hom, ← Int.cast_ofNat,
-      ← Int.coe_castRingHom, eval₂_hom, Int.coe_castRingHom, ZMod.int_coe_zMod_eq_zero_iff_dvd _ _]
+      ← Int.coe_castRingHom, eval₂_hom, Int.coe_castRingHom, ZMod.int_cast_zmod_eq_zero_iff_dvd _ _]
     apply Int.dvd_natAbs.1
     exact_mod_cast min_fac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
   have hpb : ¬p ∣ b :=

Mathbin/NumberTheory/PythagoreanTriples.lean

@@ -40,7 +40,7 @@ theorem sq_ne_two_fin_zMod_four (z : ZMod 4) : z * z ≠ 2 :=
 theorem Int.sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2 :=
   by
   suffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by norm_num at this
-  rw [← ZMod.int_coe_eq_int_coe_iff']
+  rw [← ZMod.int_cast_eq_int_cast_iff']
   simpa using sq_ne_two_fin_zMod_four _
 #align int.sq_ne_two_mod_four Int.sq_ne_two_mod_four
 

Mathbin/NumberTheory/Wilson.lean

@@ -46,7 +46,7 @@ theorem prime_of_fac_equiv_neg_one (h : ((n - 1)! : ZMod n) = -1) (h1 : n ≠ 1)
   obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2
   have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)
   refine' hm2.ne' (nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans _)))
-  rw [← ZMod.nat_coe_zMod_eq_zero_iff_dvd, cast_add, cast_one, h, add_left_neg]
+  rw [← ZMod.nat_cast_zmod_eq_zero_iff_dvd, cast_add, cast_one, h, add_left_neg]
 #align nat.prime_of_fac_equiv_neg_one Nat.prime_of_fac_equiv_neg_one
 
 /-- **Wilson's Theorem**: For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` iff n is prime. -/

Mathbin/NumberTheory/Zsqrtd/GaussianInt.lean

@@ -310,7 +310,7 @@ theorem mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact p.Prime]
         generalize p % 4 = m; decide!
       let ⟨k, hk⟩ := ZMod.exists_sq_eq_neg_one_iff.2 <| by rw [hp41] <;> exact by decide
       obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ)(h : k' < p), (k' : ZMod p) = k := by
-        refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zMod_val k⟩
+        refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩
       have hpk : p ∣ k ^ 2 + 1 := by
         rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
           ← hk, add_left_neg]