bump to nightly-2023-04-06-02

mathlib commit leanprover-community/mathlib@06a655b

Mathbin/Algebra/Divisibility/Basic.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston,
 Neil Strickland, Aaron Anderson
 
 ! This file was ported from Lean 3 source module algebra.divisibility.basic
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -180,7 +180,7 @@ end Semigroup
 
 section Monoid
 
-variable [Monoid α]
+variable [Monoid α] {a b : α}
 
 #print dvd_refl /-
 @[refl, simp]
@@ -208,6 +208,12 @@ theorem one_dvd (a : α) : 1 ∣ a :=
   Dvd.intro a (one_mul a)
 #align one_dvd one_dvd
 
+theorem dvd_of_eq (h : a = b) : a ∣ b := by rw [h]
+#align dvd_of_eq dvd_of_eq
+
+alias dvd_of_eq ← Eq.dvd
+#align eq.dvd Eq.dvd
+
 end Monoid
 
 section CommSemigroup

Mathbin/Algebra/EuclideanDomain/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.euclidean_domain.basic
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -97,7 +97,7 @@ theorem mod_self (a : R) : a % a = 0 :=
 
 #print EuclideanDomain.dvd_mod_iff /-
 theorem dvd_mod_iff {a b c : R} (h : c ∣ b) : c ∣ a % b ↔ c ∣ a := by
-  rw [dvd_add_iff_right (h.mul_right _), div_add_mod]
+  rw [← dvd_add_right (h.mul_right _), div_add_mod]
 #align euclidean_domain.dvd_mod_iff EuclideanDomain.dvd_mod_iff
 -/
 

Mathbin/Algebra/Group/Units.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johannes Hölzl, Chris Hughes, Jens Wagemaker, Jon Eugster
 
 ! This file was ported from Lean 3 source module algebra.group.units
-! leanprover-community/mathlib commit 369525b73f229ccd76a6ec0e0e0bf2be57599768
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -853,6 +853,29 @@ theorem divp_mul_divp (x y : α) (ux uy : αˣ) : x /ₚ ux * (y /ₚ uy) = x *
   rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]
 #align divp_mul_divp divp_mul_divp
 
+variable [Subsingleton αˣ] {a b : α}
+
+@[to_additive]
+theorem eq_one_of_mul_right (h : a * b = 1) : a = 1 :=
+  congr_arg Units.inv <| Subsingleton.elim (Units.mk _ _ (by rwa [mul_comm]) h) 1
+#align eq_one_of_mul_right eq_one_of_mul_right
+#align eq_zero_of_add_right eq_zero_of_add_right
+
+@[to_additive]
+theorem eq_one_of_mul_left (h : a * b = 1) : b = 1 :=
+  congr_arg Units.inv <| Subsingleton.elim (Units.mk _ _ h <| by rwa [mul_comm]) 1
+#align eq_one_of_mul_left eq_one_of_mul_left
+#align eq_zero_of_add_left eq_zero_of_add_left
+
+@[simp, to_additive]
+theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
+  ⟨fun h => ⟨eq_one_of_mul_right h, eq_one_of_mul_left h⟩,
+    by
+    rintro ⟨rfl, rfl⟩
+    exact mul_one _⟩
+#align mul_eq_one mul_eq_one
+#align add_eq_zero add_eq_zero
+
 end CommMonoid
 
 /-!

Mathbin/Algebra/GroupWithZero/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module algebra.group_with_zero.basic
-! leanprover-community/mathlib commit 2196ab363eb097c008d4497125e0dde23fb36db2
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -340,6 +340,24 @@ theorem mul_left_eq_self₀ : a * b = b ↔ a = 1 ∨ b = 0 :=
 
 #align mul_left_eq_self₀ mul_left_eq_self₀
 
+@[simp]
+theorem mul_eq_left₀ (ha : a ≠ 0) : a * b = a ↔ b = 1 := by
+  rw [Iff.comm, ← mul_right_inj' ha, mul_one]
+#align mul_eq_left₀ mul_eq_left₀
+
+@[simp]
+theorem mul_eq_right₀ (hb : b ≠ 0) : a * b = b ↔ a = 1 := by
+  rw [Iff.comm, ← mul_left_inj' hb, one_mul]
+#align mul_eq_right₀ mul_eq_right₀
+
+@[simp]
+theorem left_eq_mul₀ (ha : a ≠ 0) : a = a * b ↔ b = 1 := by rw [eq_comm, mul_eq_left₀ ha]
+#align left_eq_mul₀ left_eq_mul₀
+
+@[simp]
+theorem right_eq_mul₀ (hb : b ≠ 0) : b = a * b ↔ a = 1 := by rw [eq_comm, mul_eq_right₀ hb]
+#align right_eq_mul₀ right_eq_mul₀
+
 /- warning: eq_zero_of_mul_eq_self_right -> eq_zero_of_mul_eq_self_right is a dubious translation:
 lean 3 declaration is
   forall {M₀ : Type.{u1}} [_inst_1 : CancelMonoidWithZero.{u1} M₀] {a : M₀} {b : M₀}, (Ne.{succ u1} M₀ b (OfNat.ofNat.{u1} M₀ 1 (OfNat.mk.{u1} M₀ 1 (One.one.{u1} M₀ (MulOneClass.toHasOne.{u1} M₀ (MulZeroOneClass.toMulOneClass.{u1} M₀ (MonoidWithZero.toMulZeroOneClass.{u1} M₀ (CancelMonoidWithZero.toMonoidWithZero.{u1} M₀ _inst_1)))))))) -> (Eq.{succ u1} M₀ (HMul.hMul.{u1, u1, u1} M₀ M₀ M₀ (instHMul.{u1} M₀ (MulZeroClass.toHasMul.{u1} M₀ (MulZeroOneClass.toMulZeroClass.{u1} M₀ (MonoidWithZero.toMulZeroOneClass.{u1} M₀ (CancelMonoidWithZero.toMonoidWithZero.{u1} M₀ _inst_1))))) a b) a) -> (Eq.{succ u1} M₀ a (OfNat.ofNat.{u1} M₀ 0 (OfNat.mk.{u1} M₀ 0 (Zero.zero.{u1} M₀ (MulZeroClass.toHasZero.{u1} M₀ (MulZeroOneClass.toMulZeroClass.{u1} M₀ (MonoidWithZero.toMulZeroOneClass.{u1} M₀ (CancelMonoidWithZero.toMonoidWithZero.{u1} M₀ _inst_1))))))))
@@ -494,6 +512,17 @@ instance (priority := 100) GroupWithZero.toDivisionMonoid : DivisionMonoid G₀
 #align group_with_zero.to_division_monoid GroupWithZero.toDivisionMonoid
 -/
 
+-- see Note [lower instance priority]
+instance (priority := 10) GroupWithZero.toCancelMonoidWithZero : CancelMonoidWithZero G₀ :=
+  {
+    ‹GroupWithZero
+        G₀› with
+    mul_left_cancel_of_ne_zero := fun x y z hx h => by
+      rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]
+    mul_right_cancel_of_ne_zero := fun x y z hy h => by
+      rw [← mul_inv_cancel_right₀ hy x, h, mul_inv_cancel_right₀ hy z] }
+#align group_with_zero.to_cancel_monoid_with_zero GroupWithZero.toCancelMonoidWithZero
+
 end GroupWithZero
 
 section GroupWithZero

Mathbin/Algebra/GroupWithZero/Divisibility.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston,
 Neil Strickland, Aaron Anderson
 
 ! This file was ported from Lean 3 source module algebra.group_with_zero.divisibility
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -159,3 +159,37 @@ theorem ne_zero_of_dvd_ne_zero {p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) : p
 
 end MonoidWithZero
 
+section CancelCommMonoidWithZero
+
+variable [CancelCommMonoidWithZero α] [Subsingleton αˣ] {a b : α}
+
+theorem dvd_antisymm : a ∣ b → b ∣ a → a = b :=
+  by
+  rintro ⟨c, rfl⟩ ⟨d, hcd⟩
+  rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
+  obtain ⟨rfl, -⟩ | rfl := hcd <;> simp
+#align dvd_antisymm dvd_antisymm
+
+attribute [protected] Nat.dvd_antisymm
+
+--This lemma is in core, so we protect it here
+theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
+  flip dvd_antisymm
+#align dvd_antisymm' dvd_antisymm'
+
+alias dvd_antisymm ← Dvd.Dvd.antisymm
+#align has_dvd.dvd.antisymm Dvd.Dvd.antisymm
+
+alias dvd_antisymm' ← Dvd.Dvd.antisymm'
+#align has_dvd.dvd.antisymm' Dvd.Dvd.antisymm'
+
+theorem eq_of_forall_dvd (h : ∀ c, a ∣ c ↔ b ∣ c) : a = b :=
+  ((h _).2 dvd_rfl).antisymm <| (h _).1 dvd_rfl
+#align eq_of_forall_dvd eq_of_forall_dvd
+
+theorem eq_of_forall_dvd' (h : ∀ c, c ∣ a ↔ c ∣ b) : a = b :=
+  ((h _).1 dvd_rfl).antisymm <| (h _).2 dvd_rfl
+#align eq_of_forall_dvd' eq_of_forall_dvd'
+
+end CancelCommMonoidWithZero
+

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 7aac545b979fe3ffab5c93b833129e5c8d826296
+! leanprover-community/mathlib commit 039a089d2a4b93c761b234f3e5f5aeb752bac60f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -201,10 +201,10 @@ section StrongRankCondition
 variable {α : Type _} [CommRing α] [StrongRankCondition α] (E : LinearRecurrence α)
 
 /-- The dimension of `E.sol_space` is `E.order`. -/
-theorem solSpace_dim : Module.rank α E.solSpace = E.order :=
+theorem solSpace_rank : Module.rank α E.solSpace = E.order :=
   letI := nontrivial_of_invariantBasisNumber α
-  @dim_fin_fun α _ _ E.order ▸ E.to_init.dim_eq
-#align linear_recurrence.sol_space_dim LinearRecurrence.solSpace_dim
+  @rank_fin_fun α _ _ E.order ▸ E.to_init.rank_eq
+#align linear_recurrence.sol_space_rank LinearRecurrence.solSpace_rank
 
 end StrongRankCondition
 

Mathbin/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 
 ! This file was ported from Lean 3 source module algebra.order.monoid.canonical.defs
-! leanprover-community/mathlib commit de87d5053a9fe5cbde723172c0fb7e27e7436473
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -351,6 +351,8 @@ lean 3 declaration is
 but is expected to have type
   forall {α : Type.{u1}} [_inst_1 : CanonicallyOrderedMonoid.{u1} α] {a : α} {b : α}, Iff (Eq.{succ u1} α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α (Monoid.toMulOneClass.{u1} α (CommMonoid.toMonoid.{u1} α (OrderedCommMonoid.toCommMonoid.{u1} α (CanonicallyOrderedMonoid.toOrderedCommMonoid.{u1} α _inst_1)))))) a b) (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (Monoid.toOne.{u1} α (CommMonoid.toMonoid.{u1} α (OrderedCommMonoid.toCommMonoid.{u1} α (CanonicallyOrderedMonoid.toOrderedCommMonoid.{u1} α _inst_1))))))) (And (Eq.{succ u1} α a (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (Monoid.toOne.{u1} α (CommMonoid.toMonoid.{u1} α (OrderedCommMonoid.toCommMonoid.{u1} α (CanonicallyOrderedMonoid.toOrderedCommMonoid.{u1} α _inst_1))))))) (Eq.{succ u1} α b (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (Monoid.toOne.{u1} α (CommMonoid.toMonoid.{u1} α (OrderedCommMonoid.toCommMonoid.{u1} α (CanonicallyOrderedMonoid.toOrderedCommMonoid.{u1} α _inst_1))))))))
 Case conversion may be inaccurate. Consider using '#align mul_eq_one_iff mul_eq_one_iffₓ'. -/
+--TODO: This is a special case of `mul_eq_one`. We need the instance
+-- `canonically_ordered_monoid α → unique αˣ`
 @[simp, to_additive]
 theorem mul_eq_one_iff : a * b = 1 ↔ a = 1 ∧ b = 1 :=
   mul_eq_one_iff' (one_le _) (one_le _)

Mathbin/Algebra/Quaternion.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module algebra.quaternion
-! leanprover-community/mathlib commit da3fc4a33ff6bc75f077f691dc94c217b8d41559
+! leanprover-community/mathlib commit 039a089d2a4b93c761b234f3e5f5aeb752bac60f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -513,17 +513,17 @@ instance : Module.Finite R ℍ[R,c₁,c₂] :=
 instance : Module.Free R ℍ[R,c₁,c₂] :=
   Module.Free.of_basis (basisOneIJK c₁ c₂)
 
-theorem dim_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂] = 4 :=
+theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂] = 4 :=
   by
-  rw [dim_eq_card_basis (basis_one_i_j_k c₁ c₂), Fintype.card_fin]
+  rw [rank_eq_card_basis (basis_one_i_j_k c₁ c₂), Fintype.card_fin]
   norm_num
-#align quaternion_algebra.dim_eq_four QuaternionAlgebra.dim_eq_four
+#align quaternion_algebra.rank_eq_four QuaternionAlgebra.rank_eq_four
 
 theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4 :=
   by
   have : Cardinal.toNat 4 = 4 := by
     rw [← Cardinal.toNat_cast 4, Nat.cast_bit0, Nat.cast_bit0, Nat.cast_one]
-  rw [FiniteDimensional.finrank, dim_eq_four, this]
+  rw [FiniteDimensional.finrank, rank_eq_four, this]
 #align quaternion_algebra.finrank_eq_four QuaternionAlgebra.finrank_eq_four
 
 end
@@ -1210,9 +1210,9 @@ instance : Module.Finite R ℍ[R] :=
 instance : Module.Free R ℍ[R] :=
   QuaternionAlgebra.Module.free _ _
 
-theorem dim_eq_four [StrongRankCondition R] : Module.rank R ℍ[R] = 4 :=
-  QuaternionAlgebra.dim_eq_four _ _
-#align quaternion.dim_eq_four Quaternion.dim_eq_four
+theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R] = 4 :=
+  QuaternionAlgebra.rank_eq_four _ _
+#align quaternion.rank_eq_four Quaternion.rank_eq_four
 
 theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R] = 4 :=
   QuaternionAlgebra.finrank_eq_four _ _

Mathbin/Algebra/Ring/BooleanRing.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Yaël Dillies
 
 ! This file was ported from Lean 3 source module algebra.ring.boolean_ring
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -84,12 +84,12 @@ theorem neg_eq : -a = a :=
 
 #align neg_eq neg_eq
 
-theorem add_eq_zero : a + b = 0 ↔ a = b :=
+theorem add_eq_zero' : a + b = 0 ↔ a = b :=
   calc
     a + b = 0 ↔ a = -b := add_eq_zero_iff_eq_neg
     _ ↔ a = b := by rw [neg_eq]
 
-#align add_eq_zero add_eq_zero
+#align add_eq_zero' add_eq_zero'
 
 @[simp]
 theorem mul_add_mul : a * b + b * a = 0 :=
@@ -114,7 +114,8 @@ theorem mul_one_add_self : a * (1 + a) = 0 := by rw [mul_add, mul_one, mul_self,
 
 -- Note [lower instance priority]
 instance (priority := 100) BooleanRing.toCommRing : CommRing α :=
-  { (inferInstance : BooleanRing α) with mul_comm := fun a b => by rw [← add_eq_zero, mul_add_mul] }
+  { (inferInstance : BooleanRing α) with
+    mul_comm := fun a b => by rw [← add_eq_zero', mul_add_mul] }
 #align boolean_ring.to_comm_ring BooleanRing.toCommRing
 
 end BooleanRing