Skip to content

Commit efe2593

Browse files
alreadydonealreadydone
authored
Merge branch 'master' into Submodule.SMul
2 parents d3c5b98 + d7abea9 commit efe2593

30 files changed

Lines changed: 1338 additions & 70 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4431,10 +4431,13 @@ import Mathlib.RingTheory.MaximalSpectrum
44314431
import Mathlib.RingTheory.Multiplicity
44324432
import Mathlib.RingTheory.MvPolynomial
44334433
import Mathlib.RingTheory.MvPolynomial.Basic
4434+
import Mathlib.RingTheory.MvPolynomial.EulerIdentity
44344435
import Mathlib.RingTheory.MvPolynomial.FreeCommRing
4436+
import Mathlib.RingTheory.MvPolynomial.Groebner
44354437
import Mathlib.RingTheory.MvPolynomial.Homogeneous
44364438
import Mathlib.RingTheory.MvPolynomial.Ideal
44374439
import Mathlib.RingTheory.MvPolynomial.Localization
4440+
import Mathlib.RingTheory.MvPolynomial.MonomialOrder
44384441
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
44394442
import Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
44404443
import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

‎Mathlib/Algebra/GCDMonoid/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1315,8 +1315,8 @@ namespace Associates
13151315
variable [CancelCommMonoidWithZero α] [GCDMonoid α]
13161316

13171317
instance instGCDMonoid : GCDMonoid (Associates α) where
1318-
gcd := Quotient.map₂' gcd fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.gcd hb
1319-
lcm := Quotient.map₂' lcm fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.lcm hb
1318+
gcd := Quotient.map₂ gcd fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.gcd hb
1319+
lcm := Quotient.map₂ lcm fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.lcm hb
13201320
gcd_dvd_left := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_left _ _)
13211321
gcd_dvd_right := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_right _ _)
13221322
dvd_gcd := by

‎Mathlib/Algebra/MvPolynomial/Degrees.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -500,6 +500,15 @@ theorem coeff_eq_zero_of_totalDegree_lt {f : MvPolynomial σ R} {d : σ →₀
500500
exact lt_irrefl _
501501
· exact lt_of_le_of_lt (Nat.zero_le _) h
502502

503+
theorem totalDegree_eq_zero_iff_eq_C {p : MvPolynomial σ R} :
504+
p.totalDegree = 0 ↔ p = C (p.coeff 0) := by
505+
constructor <;> intro h
506+
· ext m; classical rw [coeff_C]; split_ifs with hm; · rw [← hm]
507+
apply coeff_eq_zero_of_totalDegree_lt; rw [h]
508+
exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
509+
(Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)
510+
· rw [h, totalDegree_C]
511+
503512
theorem totalDegree_rename_le (f : σ → τ) (p : MvPolynomial σ R) :
504513
(rename f p).totalDegree ≤ p.totalDegree :=
505514
Finset.sup_le fun b => by

‎Mathlib/Algebra/MvPolynomial/PDeriv.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,13 @@ theorem pderiv_monomial {i : σ} :
7272
· rw [Finsupp.not_mem_support_iff] at hi; simp [hi]
7373
· simp
7474

75+
lemma X_mul_pderiv_monomial {i : σ} {m : σ →₀ ℕ} {r : R} :
76+
X i * pderiv i (monomial m r) = m i • monomial m r := by
77+
rw [pderiv_monomial, X, monomial_mul, smul_monomial]
78+
by_cases h : m i = 0
79+
· simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]
80+
rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]
81+
7582
theorem pderiv_C {i : σ} : pderiv i (C a) = 0 :=
7683
derivation_C _ _
7784

‎Mathlib/Algebra/Polynomial/FieldDivision.lean‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -175,11 +175,10 @@ See `isRoot_of_isRoot_iff_dvd_derivative_mul` -/
175175
theorem isRoot_of_isRoot_of_dvd_derivative_mul [CharZero R] {f g : R[X]} (hf0 : f ≠ 0)
176176
(hfd : f ∣ f.derivative * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a := by
177177
rcases hfd with ⟨r, hr⟩
178-
by_cases hdf0 : derivative f = 0
179-
· rw [eq_C_of_derivative_eq_zero hdf0] at haf hf0
180-
simp only [eval_C, derivative_C, zero_mul, dvd_zero, iff_true, IsRoot.def] at haf
181-
rw [haf, map_zero] at hf0
182-
exact (hf0 rfl).elim
178+
have hdf0 : derivative f ≠ 0 := by
179+
contrapose! haf
180+
rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
181+
exact not_isRoot_C _ _ <| C_ne_zero.mp hf0
183182
by_contra hg
184183
have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)
185184
have hr' := congr_arg (rootMultiplicity a) hr

‎Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,18 @@ theorem U_complex_cos (n : ℤ) : (U ℂ n).eval (cos θ) * sin θ = sin ((n + 1
9494
push_cast
9595
ring_nf
9696

97+
/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
98+
`2 * cos θ` to the value `2 * cos (n * θ)`. -/
99+
@[simp]
100+
theorem C_two_mul_complex_cos (n : ℤ) : (C ℂ n).eval (2 * cos θ) = 2 * cos (n * θ) := by
101+
simp [C_eq_two_mul_T_comp_half_mul_X]
102+
103+
/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
104+
evaluates on `2 * cos θ` to the value `sin ((n + 1) * θ) / sin θ`. -/
105+
@[simp]
106+
theorem S_two_mul_complex_cos (n : ℤ) : (S ℂ n).eval (2 * cos θ) * sin θ = sin ((n + 1) * θ) := by
107+
simp [S_eq_U_comp_half_mul_X]
108+
97109
end Complex
98110

99111
/-! ### Real versions -/
@@ -115,6 +127,18 @@ value `sin ((n + 1) * θ) / sin θ`. -/
115127
theorem U_real_cos : (U ℝ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) :=
116128
mod_cast U_complex_cos θ n
117129

130+
/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
131+
`2 * cos θ` to the value `2 * cos (n * θ)`. -/
132+
@[simp]
133+
theorem C_two_mul_real_cos : (C ℝ n).eval (2 * cos θ) = 2 * cos (n * θ) := by
134+
simp [C_eq_two_mul_T_comp_half_mul_X]
135+
136+
/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
137+
evaluates on `2 * cos θ` to the value `sin ((n + 1) * θ) / sin θ`. -/
138+
@[simp]
139+
theorem S_two_mul_real_cos : (S ℝ n).eval (2 * cos θ) * sin θ = sin ((n + 1) * θ) := by
140+
simp [S_eq_U_comp_half_mul_X]
141+
118142
end Real
119143

120144
end Polynomial.Chebyshev

‎Mathlib/Combinatorics/SimpleGraph/Matching.lean‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -333,11 +333,9 @@ to the same vertex.
333333
lemma IsCycles.other_adj_of_adj (h : G.IsCycles) (hadj : G.Adj v w) :
334334
∃ w', w ≠ w' ∧ G.Adj v w' := by
335335
simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢
336-
cases' (G.neighborSet v).eq_empty_or_nonempty with hl hr
337-
· exact ((Set.eq_empty_iff_forall_not_mem.mp hl) _ hadj).elim
338-
· have := h hr
339-
obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by omega) w
340-
exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩
336+
have := h ⟨w, hadj⟩
337+
obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by omega) w
338+
exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩
341339

342340
open scoped symmDiff
343341

‎Mathlib/Data/Finset/Lattice/Fold.lean‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -634,6 +634,22 @@ protected theorem sup_lt_iff (ha : ⊥ < a) : s.sup f < a ↔ ∀ b ∈ s, f b <
634634
Finset.cons_induction_on s (fun _ => ha) fun c t hc => by
635635
simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right⟩
636636

637+
theorem sup_mem_of_nonempty (hs : s.Nonempty) : s.sup f ∈ f '' s := by
638+
classical
639+
induction s using Finset.induction with
640+
| empty => exfalso; simp only [Finset.not_nonempty_empty] at hs
641+
| @insert a s _ h =>
642+
rw [Finset.sup_insert (b := a) (s := s) (f := f)]
643+
by_cases hs : s = ∅
644+
· simp [hs]
645+
· rw [← ne_eq, ← Finset.nonempty_iff_ne_empty] at hs
646+
simp only [Finset.coe_insert]
647+
rcases le_total (f a) (s.sup f) with (ha | ha)
648+
· rw [sup_eq_right.mpr ha]
649+
exact Set.image_mono (Set.subset_insert a s) (h hs)
650+
· rw [sup_eq_left.mpr ha]
651+
apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)
652+
637653
end OrderBot
638654

639655
section OrderTop

‎Mathlib/Data/Finsupp/MonomialOrder.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,6 @@ example : toLex (Finsupp.single 1 1) < toLex (Finsupp.single 0 1) := by
135135
example : toLex (Finsupp.single 1 1) < toLex (Finsupp.single 0 2) := by
136136
use 0; simp
137137

138-
139138
variable {σ : Type*} [LinearOrder σ]
140139

141140
/-- The lexicographic order on `σ →₀ ℕ`, as a `MonomialOrder` -/

‎Mathlib/Data/Finsupp/Order.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -322,6 +322,10 @@ theorem add_sub_single_one {a : ι} {u u' : ι →₀ ℕ} (h : u' a ≠ 0) :
322322
u + (u' - single a 1) = u + u' - single a 1 :=
323323
(add_tsub_assoc_of_le (single_le_iff.mpr <| Nat.one_le_iff_ne_zero.mpr h) _).symm
324324

325+
lemma sub_add_single_one_cancel {u : ι →₀ ℕ} {i : ι} (h : u i ≠ 0) :
326+
u - single i 1 + single i 1 = u := by
327+
rw [sub_single_one_add h, add_tsub_cancel_right]
328+
325329
end Nat
326330

327331
end Finsupp

0 commit comments

Comments
 (0)