Merge branch 'master' into IsSelfAdjoint-structure

Author: j-loreaux

Mathlib.lean

@@ -2755,6 +2755,7 @@ import Mathlib.Combinatorics.Quiver.Cast
 import Mathlib.Combinatorics.Quiver.ConnectedComponent
 import Mathlib.Combinatorics.Quiver.Covering
 import Mathlib.Combinatorics.Quiver.Path
+import Mathlib.Combinatorics.Quiver.Path.Weight
 import Mathlib.Combinatorics.Quiver.Prefunctor
 import Mathlib.Combinatorics.Quiver.Push
 import Mathlib.Combinatorics.Quiver.ReflQuiver
@@ -4035,6 +4036,7 @@ import Mathlib.LinearAlgebra.Dimension.Subsingleton
 import Mathlib.LinearAlgebra.Dimension.Torsion.Basic
 import Mathlib.LinearAlgebra.Dimension.Torsion.Finite
 import Mathlib.LinearAlgebra.DirectSum.Basis
+import Mathlib.LinearAlgebra.DirectSum.Finite
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.LinearAlgebra.Dual.Basis

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -369,19 +369,9 @@ lemma prod_congr_of_eq_on_inter {ι M : Type*} {s₁ s₂ : Finset ι} {f g : ι
 theorem prod_eq_mul_of_mem {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s)
     (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x ∈ s, f x = f a * f b := by
   haveI := Classical.decEq ι; let s' := ({a, b} : Finset ι)
-  have hu : s' ⊆ s := by
-    refine insert_subset_iff.mpr ?_
-    apply And.intro ha
-    apply singleton_subset_iff.mpr hb
-  have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by
-    intro c hc hcs
-    apply h₀ c hc
-    apply not_or.mp
-    intro hab
-    apply hcs
-    rw [mem_insert, mem_singleton]
-    exact hab
-  rw [← prod_subset hu hf]
+  have hu : s' ⊆ s := by grind [Finset.insert_subset_iff, Finset.singleton_subset_iff]
+  have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by grind [Finset.mem_insert, Finset.mem_singleton]
+  rw [← Finset.prod_subset hu hf]
   exact Finset.prod_pair hn
 
 @[to_additive]

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -165,7 +165,7 @@ attribute [local simp] Mon_Class.tensorObj.one_def Mon_Class.tensorObj.mul_def i
 theorem comul_tensorObj_tensorObj_right :
     Coalgebra.comul (R := R) (A := (CoalgCat.of R M ⊗
       (CoalgCat.of R N ⊗ CoalgCat.of R P) : CoalgCat R))
-      = Coalgebra.comul (A := M ⊗[R] N ⊗[R] P) := by
+      = Coalgebra.comul (A := M ⊗[R] (N ⊗[R] P)) := by
   rw [ofComonObjCoalgebraStruct_comul]
   simp only [Comon_.monoidal_tensorObj_comon_comul]
   simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
@@ -176,7 +176,7 @@ attribute [local simp] Mon_Class.tensorObj.one_def Mon_Class.tensorObj.mul_def i
 theorem comul_tensorObj_tensorObj_left :
     Coalgebra.comul (R := R)
       (A := ((CoalgCat.of R M ⊗ CoalgCat.of R N) ⊗ CoalgCat.of R P : CoalgCat R))
-      = Coalgebra.comul (A := (M ⊗[R] N) ⊗[R] P) := by
+      = Coalgebra.comul (A := M ⊗[R] N ⊗[R] P) := by
   rw [ofComonObjCoalgebraStruct_comul]
   dsimp
   simp only [toComonObj]

Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -322,18 +322,18 @@ theorem mem_carrier {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s :=
   Iff.rfl
 
 @[to_additive (attr := simp)]
-theorem mem_mk {s : Set G} {x : G} (h_one) (h_mul) (h_inv) :
-    x ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ↔ x ∈ s :=
+theorem mem_mk {s : Submonoid G} {x : G} (h_inv) :
+    x ∈ mk s h_inv ↔ x ∈ s :=
   Iff.rfl
 
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_set_mk {s : Set G} (h_one) (h_mul) (h_inv) :
-    (mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv : Set G) = s :=
+@[to_additive (attr := simp)]
+theorem coe_set_mk {s : Submonoid G} (h_inv) :
+    (mk s h_inv : Set G) = s :=
   rfl
 
 @[to_additive (attr := simp)]
-theorem mk_le_mk {s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv') :
-    mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t :=
+theorem mk_le_mk {s t : Submonoid G} (h_inv) (h_inv') :
+    mk s h_inv ≤ mk t h_inv' ↔ s ≤ t :=
   Iff.rfl
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -293,7 +293,7 @@ theorem ker_id : (MonoidHom.id G).ker = ⊥ :=
   rfl
 
 @[to_additive] theorem ker_eq_top_iff {f : G →* M} : f.ker = ⊤ ↔ f = 1 := by
-  simp_rw [ker, ← top_le_iff, SetLike.le_def, f.ext_iff, Subgroup.mem_top, true_imp_iff]; rfl
+  simp [ker, ← top_le_iff, SetLike.le_def, f.ext_iff]
 
 @[to_additive] theorem range_eq_bot_iff {f : G →* G'} : f.range = ⊥ ↔ f = 1 := by
   rw [← le_bot_iff, f.range_eq_map, map_le_iff_le_comap, top_le_iff, comap_bot, ker_eq_top_iff]

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

@@ -72,15 +72,14 @@ theorem mul_apply_mul_eq_mul_of_uniqueMul [Mul A] {f g : MonoidAlgebra R A} {a0
   classical
   simp_rw [mul_apply, sum, ← Finset.sum_product']
   refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]
-  · refine fun ab hab hne => if_neg (fun he => hne <| Prod.ext ?_ ?_)
+  · refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
     exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]
-  · refine fun hnotMem => ite_eq_right_iff.mpr (fun _ => ?_)
+  · refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
     rcases not_and_or.mp hnotMem with af | bg
     · rw [notMem_support_iff.mp af, zero_mul]
     · rw [notMem_support_iff.mp bg, mul_zero]
 
-instance instNoZeroDivisorsOfUniqueProds [NoZeroDivisors R] [Mul A] [UniqueProds A] :
-    NoZeroDivisors (MonoidAlgebra R A) where
+instance [NoZeroDivisors R] [Mul A] [UniqueProds A] : NoZeroDivisors (MonoidAlgebra R A) where
   eq_zero_or_eq_zero_of_mul_eq_zero {a b} ab := by
     contrapose! ab
     obtain ⟨da, a0, db, b0, h⟩ := UniqueProds.uniqueMul_of_nonempty
@@ -89,6 +88,34 @@ instance instNoZeroDivisorsOfUniqueProds [NoZeroDivisors R] [Mul A] [UniqueProds
     rw [mem_support_iff] at a0 b0 ⊢
     exact mul_apply_mul_eq_mul_of_uniqueMul h ▸ mul_ne_zero a0 b0
 
+instance [IsCancelAdd R] [IsLeftCancelMulZero R] [Mul A] [UniqueProds A] :
+    IsLeftCancelMulZero (MonoidAlgebra R A) where
+  mul_left_cancel_of_ne_zero {f g₁ g₂} hf eq := by
+    classical
+    induction hg : g₁.support ∪ g₂.support using Finset.eraseInduction generalizing g₁ g₂ with
+    | _ s ih =>
+    obtain h | h := s.eq_empty_or_nonempty <;> subst s
+    · simp_rw [Finset.union_eq_empty, support_eq_empty] at h; exact h.1.trans h.2.symm
+    have ⟨af, haf, ag, hag, uniq⟩ := UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.2 hf) h
+    have h := mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
+    rw [eq, mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
+    have := mul_left_cancel₀ (mem_support_iff.mp haf) h
+    rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
+    simp_rw [mul_add, add_right_cancel_iff] at eq
+    rw [ih ag hag eq]
+    simp_rw [support_erase, Finset.erase_union_distrib]
+
+instance [IsCancelAdd R] [IsRightCancelMulZero R] [Mul A] [UniqueProds A] :
+    IsRightCancelMulZero (MonoidAlgebra R A) :=
+  MulOpposite.isLeftCancelMulZero_iff.mp <|
+    MonoidAlgebra.opRingEquiv.injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)
+
+instance [IsCancelAdd R] [IsCancelMulZero R] [Mul A] [UniqueProds A] :
+    IsCancelMulZero (MonoidAlgebra R A) where
+
+instance [IsCancelAdd R] [IsDomain R] [Monoid A] [UniqueProds A] :
+    IsDomain (MonoidAlgebra R A) where
+
 end MonoidAlgebra
 
 namespace AddMonoidAlgebra
@@ -100,26 +127,20 @@ theorem mul_apply_add_eq_mul_of_uniqueAdd [Add A] {f g : R[A]} {a0 b0 : A}
     (f * g) (a0 + b0) = f a0 * g b0 :=
   MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul (A := Multiplicative A) h
 
-instance instNoZeroDivisorsOfUniqueSums [NoZeroDivisors R] [Add A] [UniqueSums A] :
-    NoZeroDivisors R[A] := MonoidAlgebra.instNoZeroDivisorsOfUniqueProds (A := Multiplicative A)
-
-end AddMonoidAlgebra
-end Semiring
-
-section Ring
-variable [Ring R] [IsDomain R]
+instance [NoZeroDivisors R] [Add A] [UniqueSums A] : NoZeroDivisors R[A] :=
+  inferInstanceAs (NoZeroDivisors (MonoidAlgebra R (Multiplicative A)))
 
-namespace MonoidAlgebra
+instance [IsCancelAdd R] [IsLeftCancelMulZero R] [Add A] [UniqueSums A] :
+    IsLeftCancelMulZero R[A] :=
+  inferInstanceAs (IsLeftCancelMulZero (MonoidAlgebra R (Multiplicative A)))
 
-instance instIsDomainOfUniqueProds [Monoid A] [UniqueProds A] : IsDomain (MonoidAlgebra R A) :=
-  NoZeroDivisors.to_isDomain _
+instance [IsCancelAdd R] [IsRightCancelMulZero R] [Add A] [UniqueSums A] :
+    IsRightCancelMulZero R[A] :=
+  inferInstanceAs (IsRightCancelMulZero (MonoidAlgebra R (Multiplicative A)))
 
-end MonoidAlgebra
+instance [IsCancelAdd R] [IsCancelMulZero R] [Add A] [UniqueSums A] : IsCancelMulZero R[A] where
 
-namespace AddMonoidAlgebra
-
-instance instIsDomainOfUniqueSums [AddMonoid A] [UniqueSums A] : IsDomain R[A] :=
-  NoZeroDivisors.to_isDomain _
+instance [IsCancelAdd R] [IsDomain R] [AddMonoid A] [UniqueSums A] : IsDomain R[A] where
 
 end AddMonoidAlgebra
-end Ring
+end Semiring

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Algebra.Subalgebra.Lattice
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Algebra.Regular.Pow
 import Mathlib.Data.Finsupp.Antidiagonal
@@ -243,6 +244,16 @@ instance infinite_of_nonempty (σ : Type*) (R : Type*) [Nonempty σ] [CommSemiri
   Infinite.of_injective ((fun s : σ →₀ ℕ => monomial s 1) ∘ Finsupp.single (Classical.arbitrary σ))
     <| (monomial_left_injective one_ne_zero).comp (Finsupp.single_injective _)
 
+instance [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (MvPolynomial σ R) :=
+  inferInstanceAs (NoZeroDivisors (AddMonoidAlgebra ..))
+
+instance [CommSemiring R] [IsCancelAdd R] [IsCancelMulZero R] :
+    IsCancelMulZero (MvPolynomial σ R) :=
+  inferInstanceAs (IsCancelMulZero (AddMonoidAlgebra ..))
+
+/-- The multivariate polynomial ring over an integral domain is an integral domain. -/
+instance [CommSemiring R] [IsCancelAdd R] [IsDomain R] : IsDomain (MvPolynomial σ R) where
+
 theorem C_eq_coe_nat (n : ℕ) : (C ↑n : MvPolynomial σ R) = n := by
   induction n <;> simp [*]
 

Mathlib/Algebra/MvPolynomial/Funext.lean

@@ -5,9 +5,9 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Polynomial.RingDivision
 import Mathlib.Algebra.Polynomial.Roots
+import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.Algebra.MvPolynomial.Polynomial
 import Mathlib.Algebra.MvPolynomial.Rename
-import Mathlib.RingTheory.Polynomial.Basic
 
 /-!
 ## Function extensionality for multivariate polynomials

Mathlib/Algebra/Polynomial/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
-import Mathlib.Algebra.MonoidAlgebra.Defs
+import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
 import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Algebra.Ring.Action.Rat
 import Mathlib.Data.Finset.Sort
@@ -1146,7 +1146,7 @@ instance commRing [CommRing R] : CommRing R[X] :=
   { toRing := Polynomial.ring
     mul_comm := mul_comm }
 
-section NonzeroSemiring
+section Semiring
 
 variable [Semiring R]
 
@@ -1160,7 +1160,20 @@ instance nontrivial [Nontrivial R] : Nontrivial R[X] := by
 theorem X_ne_zero [Nontrivial R] : (X : R[X]) ≠ 0 :=
   mt (congr_arg fun p => coeff p 1) (by simp)
 
-end NonzeroSemiring
+instance [NoZeroDivisors R] : NoZeroDivisors R[X] :=
+  (toFinsuppIso R).injective.noZeroDivisors _ (map_zero _) (map_mul _)
+
+instance [IsCancelAdd R] [IsLeftCancelMulZero R] : IsLeftCancelMulZero R[X] :=
+  (toFinsuppIso R).injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)
+
+instance [IsCancelAdd R] [IsRightCancelMulZero R] : IsRightCancelMulZero R[X] :=
+  (toFinsuppIso R).injective.isRightCancelMulZero _ (map_zero _) (map_mul _)
+
+instance [IsCancelAdd R] [IsCancelMulZero R] : IsCancelMulZero R[X] where
+
+instance [IsCancelAdd R] [IsDomain R] : IsDomain R[X] where
+
+end Semiring
 
 section DivisionSemiring
 variable [DivisionSemiring R]

Mathlib/Algebra/Polynomial/Degree/Domain.lean

@@ -30,12 +30,6 @@ section Semiring
 
 variable [Semiring R] [NoZeroDivisors R] {p q : R[X]}
 
-instance : NoZeroDivisors R[X] where
-  eq_zero_or_eq_zero_of_mul_eq_zero h := by
-    rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero]
-    refine eq_zero_or_eq_zero_of_mul_eq_zero ?_
-    rw [← leadingCoeff_zero, ← leadingCoeff_mul, h]
-
 lemma natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p*q).natDegree = p.natDegree + q.natDegree := by
   rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
     Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]
@@ -97,11 +91,4 @@ lemma natDegree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : R[X]} (hp₁ : p₁ ≠
 
 end Semiring
 
-section Ring
-
-variable [Ring R] [Nontrivial R] [IsDomain R] {p q : R[X]}
-
-instance : IsDomain R[X] := NoZeroDivisors.to_isDomain _
-
-end Ring
 end Polynomial