bump to nightly-2023-04-04-02

mathlib commit leanprover-community/mathlib@3cacc94

Mathbin/Algebra/Category/Group/Preadditive.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 
 ! This file was ported from Lean 3 source module algebra.category.Group.preadditive
-! leanprover-community/mathlib commit 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Preadditive.Basic
 
 /-!
 # The category of additive commutative groups is preadditive.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 

Mathbin/Algebra/Category/Group/Zero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.category.Group.zero
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.Limits.Shapes.ZeroObjects
 /-!
 # The category of (commutative) (additive) groups has a zero object.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `AddCommGroup` also has zero morphisms. For definitional reasons, we infer this from preadditivity
 rather than from the existence of a zero object.
 -/

Mathbin/Algebra/Category/Module/Projective.lean

@@ -59,7 +59,7 @@ theorem projective_of_free {ι : Type _} (b : Basis ι R M) : Projective M :=
     module. -/
 instance moduleCat_enoughProjectives : EnoughProjectives (ModuleCat.{max u v} R)
     where presentation M :=
-    ⟨{  P := ModuleCat.of R (M →₀ R)
+    ⟨{  p := ModuleCat.of R (M →₀ R)
         Projective := projective_of_free Finsupp.basisSingleOne
         f := Finsupp.basisSingleOne.constr ℕ id
         Epi :=

Mathbin/Algebra/CharP/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Joey van Langen, Casper Putz
 
 ! This file was ported from Lean 3 source module algebra.char_p.basic
-! leanprover-community/mathlib commit 10bf4f825ad729c5653adc039dafa3622e7f93c9
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -211,16 +211,17 @@ theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a
     rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
 #align char_p.int_cast_eq_zero_iff CharP.int_cast_eq_zero_iff
 
-/- warning: char_p.int_coe_eq_int_coe_iff -> CharP.int_cast_eq_int_cast_iff is a dubious translation:
-lean 3 declaration is
-  forall (R : Type.{u1}) [_inst_1 : AddGroupWithOne.{u1} R] (p : Nat) [_inst_2 : CharP.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R _inst_1) p] (a : Int) (b : Int), Iff (Eq.{succ u1} R ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Int R (HasLiftT.mk.{1, succ u1} Int R (CoeTCₓ.coe.{1, succ u1} Int R (Int.castCoe.{u1} R (AddGroupWithOne.toHasIntCast.{u1} R _inst_1)))) a) ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Int R (HasLiftT.mk.{1, succ u1} Int R (CoeTCₓ.coe.{1, succ u1} Int R (Int.castCoe.{u1} R (AddGroupWithOne.toHasIntCast.{u1} R _inst_1)))) b)) (Int.ModEq ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) p) a b)
-but is expected to have type
-  forall (R : Type.{u1}) [_inst_1 : AddGroupWithOne.{u1} R] (p : Nat) [_inst_2 : CharP.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R _inst_1) p] (a : Int) (b : Int), Iff (Eq.{succ u1} R (Int.cast.{u1} R (AddGroupWithOne.toIntCast.{u1} R _inst_1) a) (Int.cast.{u1} R (AddGroupWithOne.toIntCast.{u1} R _inst_1) b)) (Int.ModEq (Nat.cast.{0} Int instNatCastInt p) a b)
-Case conversion may be inaccurate. Consider using '#align char_p.int_coe_eq_int_coe_iff CharP.int_cast_eq_int_cast_iffₓ'. -/
-theorem CharP.int_cast_eq_int_cast_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a b : ℤ) :
-    (a : R) = (b : R) ↔ a ≡ b [ZMOD p] := by
+theorem CharP.int_cast_eq_int_cast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℤ} :
+    (a : R) = b ↔ a ≡ b [ZMOD p] := by
   rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
-#align char_p.int_coe_eq_int_coe_iff CharP.int_cast_eq_int_cast_iff
+#align char_p.int_cast_eq_int_cast CharP.int_cast_eq_int_cast
+
+theorem CharP.nat_cast_eq_nat_cast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} :
+    (a : R) = b ↔ a ≡ b [MOD p] :=
+  by
+  rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
+  exact (CharP.int_cast_eq_int_cast _ _).trans Int.coe_nat_modEq_iff
+#align char_p.nat_cast_eq_nat_cast CharP.nat_cast_eq_nat_cast
 
 #print CharP.eq /-
 theorem CharP.eq [AddMonoidWithOne R] {p q : ℕ} (c1 : CharP R p) (c2 : CharP R q) : p = q :=
@@ -452,16 +453,6 @@ theorem sub_pow_char_pow [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] {n :
   sub_pow_char_pow_of_commute _ _ _ (Commute.all _ _)
 #align sub_pow_char_pow sub_pow_char_pow
 
-/- warning: eq_iff_modeq_int -> eq_iff_modEq_int is a dubious translation:
-lean 3 declaration is
-  forall (R : Type.{u1}) [_inst_1 : Ring.{u1} R] (p : Nat) [_inst_2 : CharP.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1))) p] (a : Int) (b : Int), Iff (Eq.{succ u1} R ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Int R (HasLiftT.mk.{1, succ u1} Int R (CoeTCₓ.coe.{1, succ u1} Int R (Int.castCoe.{u1} R (AddGroupWithOne.toHasIntCast.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1)))))) a) ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Int R (HasLiftT.mk.{1, succ u1} Int R (CoeTCₓ.coe.{1, succ u1} Int R (Int.castCoe.{u1} R (AddGroupWithOne.toHasIntCast.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1)))))) b)) (Int.ModEq ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat Int (HasLiftT.mk.{1, 1} Nat Int (CoeTCₓ.coe.{1, 1} Nat Int (coeBase.{1, 1} Nat Int Int.hasCoe))) p) a b)
-but is expected to have type
-  forall (R : Type.{u1}) [_inst_1 : Ring.{u1} R] (p : Nat) [_inst_2 : CharP.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R (Ring.toAddGroupWithOne.{u1} R _inst_1)) p] (a : Int) (b : Int), Iff (Eq.{succ u1} R (Int.cast.{u1} R (Ring.toIntCast.{u1} R _inst_1) a) (Int.cast.{u1} R (Ring.toIntCast.{u1} R _inst_1) b)) (Int.ModEq (Nat.cast.{0} Int instNatCastInt p) a b)
-Case conversion may be inaccurate. Consider using '#align eq_iff_modeq_int eq_iff_modEq_intₓ'. -/
-theorem eq_iff_modEq_int [Ring R] (p : ℕ) [CharP R p] (a b : ℤ) : (a : R) = b ↔ a ≡ b [ZMOD p] := by
-  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
-#align eq_iff_modeq_int eq_iff_modEq_int
-
 /- warning: char_p.neg_one_ne_one -> CharP.neg_one_ne_one is a dubious translation:
 lean 3 declaration is
   forall (R : Type.{u1}) [_inst_1 : Ring.{u1} R] (p : Nat) [_inst_2 : CharP.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1))) p] [_inst_3 : Fact (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))) p)], Ne.{succ u1} R (Neg.neg.{u1} R (SubNegMonoid.toHasNeg.{u1} R (AddGroup.toSubNegMonoid.{u1} R (AddGroupWithOne.toAddGroup.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1))))) (OfNat.ofNat.{u1} R 1 (OfNat.mk.{u1} R 1 (One.one.{u1} R (AddMonoidWithOne.toOne.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1)))))))) (OfNat.ofNat.{u1} R 1 (OfNat.mk.{u1} R 1 (One.one.{u1} R (AddMonoidWithOne.toOne.{u1} R (AddGroupWithOne.toAddMonoidWithOne.{u1} R (AddCommGroupWithOne.toAddGroupWithOne.{u1} R (Ring.toAddCommGroupWithOne.{u1} R _inst_1)))))))

Mathbin/Algebra/CharP/Quotient.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Eric Wieser
 
 ! This file was ported from Lean 3 source module algebra.char_p.quotient
-! leanprover-community/mathlib commit 85e3c05a94b27c84dc6f234cf88326d5e0096ec3
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.RingTheory.Ideal.Quotient
 
 /-!
 # Characteristic of quotients rings
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 

Mathbin/Algebra/CubicDiscriminant.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Kurniadi Angdinata
 
 ! This file was ported from Lean 3 source module algebra.cubic_discriminant
-! leanprover-community/mathlib commit 930133160e24036d5242039fe4972407cd4f1222
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Data.Polynomial.Splits
 /-!
 # Cubics and discriminants
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines cubic polynomials over a semiring and their discriminants over a splitting field.
 
 ## Main definitions

Mathbin/Algebra/GcdMonoid/Div.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 
 ! This file was ported from Lean 3 source module algebra.gcd_monoid.div
-! leanprover-community/mathlib commit b537794f8409bc9598febb79cd510b1df5f4539d
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.RingTheory.Polynomial.Content
 /-!
 # Basic results about setwise gcds on normalized gcd monoid with a division.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main results
 
 * `finset.nat.gcd_div_eq_one`: given a nonempty finset `s` and a function `f` from `s` to

Mathbin/Algebra/LinearRecurrence.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 
 ! This file was ported from Lean 3 source module algebra.linear_recurrence
-! leanprover-community/mathlib commit 85d9f2189d9489f9983c0d01536575b0233bd305
+! leanprover-community/mathlib commit 3cacc945118c8c637d89950af01da78307f59325
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -194,16 +194,19 @@ def tupleSucc : (Fin E.order → α) →ₗ[α] Fin E.order → α
 
 end CommSemiring
 
-section Field
+section StrongRankCondition
 
-variable {α : Type _} [Field α] (E : LinearRecurrence α)
+-- note: `strong_rank_condition` is the same as `nontrivial` on `comm_ring`s, but that result,
+-- `comm_ring_strong_rank_condition`, is in a much later file.
+variable {α : Type _} [CommRing α] [StrongRankCondition α] (E : LinearRecurrence α)
 
 /-- The dimension of `E.sol_space` is `E.order`. -/
 theorem solSpace_dim : Module.rank α E.solSpace = E.order :=
-  @dim_fin_fun α _ E.order ▸ E.toInit.dim_eq
+  letI := nontrivial_of_invariantBasisNumber α
+  @dim_fin_fun α _ _ _ E.order ▸ E.to_init.dim_eq
 #align linear_recurrence.sol_space_dim LinearRecurrence.solSpace_dim
 
-end Field
+end StrongRankCondition
 
 section CommRing
 

Mathbin/Algebra/MonoidAlgebra/Division.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module algebra.monoid_algebra.division
-! leanprover-community/mathlib commit 72c366d0475675f1309d3027d3d7d47ee4423951
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Data.Finsupp.Order
 /-!
 # Division of `add_monoid_algebra` by monomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is most important for when `G = ℕ` (polynomials) or `G = σ →₀ ℕ` (multivariate
 polynomials).
 

Mathbin/Algebra/Ring/Divisibility.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
 
 ! This file was ported from Lean 3 source module algebra.ring.divisibility
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -219,6 +219,9 @@ theorem dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ b - c) : a ∣ b ↔ a 
     exact eq_add_of_sub_eq rfl
 #align dvd_iff_dvd_of_dvd_sub dvd_iff_dvd_of_dvd_sub
 
+theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg, neg_sub]
+#align dvd_sub_comm dvd_sub_comm
+
 end NonUnitalRing
 
 section Ring

Mathbin/Algebra/Squarefree.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 
 ! This file was ported from Lean 3 source module algebra.squarefree
-! leanprover-community/mathlib commit c085f3044fe585c575e322bfab45b3633c48d820
+! leanprover-community/mathlib commit 00d163e35035c3577c1c79fa53b68de17781ffc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -374,3 +374,18 @@ theorem dvd_pow_iff_dvd_of_squarefree {x y : R} {n : ℕ} (hsq : Squarefree x) (
 
 end UniqueFactorizationMonoid
 
+namespace Int
+
+@[simp]
+theorem squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n := by
+  simp_rw [Squarefree, nat_abs_surjective.forall, ← nat_abs_mul, nat_abs_dvd_iff_dvd,
+    is_unit_iff_nat_abs_eq, Nat.isUnit_iff]
+#align int.squarefree_nat_abs Int.squarefree_natAbs
+
+@[simp]
+theorem squarefree_coe_nat {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n := by
+  rw [← squarefree_nat_abs, nat_abs_of_nat]
+#align int.squarefree_coe_nat Int.squarefree_coe_nat
+
+end Int
+

Mathbin/Algebra/Star/Chsh.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.star.chsh
-! leanprover-community/mathlib commit 468b141b14016d54b479eb7a0fff1e360b7e3cf6
+! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Data.Real.Sqrt
 /-!
 # The Clauser-Horne-Shimony-Holt inequality and Tsirelson's inequality.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We establish a version of the Clauser-Horne-Shimony-Holt (CHSH) inequality
 (which is a generalization of Bell's inequality).
 This is a foundational result which implies that