From 5ddc36406a961b693ca38f3931016c9077df180c Mon Sep 17 00:00:00 2001 From: Seewoo Lee Date: Thu, 26 Dec 2024 23:37:37 -0800 Subject: [PATCH] protect Polynomial.map_eq_zero --- Mathlib/Algebra/Polynomial/FieldDivision.lean | 10 +++++----- Mathlib/Algebra/Polynomial/Splits.lean | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/FieldDivision.lean b/Mathlib/Algebra/Polynomial/FieldDivision.lean index 3b5ed5bdcc23f..e5294cbb83106 100644 --- a/Mathlib/Algebra/Polynomial/FieldDivision.lean +++ b/Mathlib/Algebra/Polynomial/FieldDivision.lean @@ -255,13 +255,13 @@ theorem degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 < exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0)))) @[simp] -theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0 := by +protected theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0 := by simp only [Polynomial.ext_iff] congr! simp [map_eq_zero, coeff_map, coeff_zero] theorem map_ne_zero [Semiring S] [Nontrivial S] {f : R →+* S} (hp : p ≠ 0) : p.map f ≠ 0 := - mt (map_eq_zero f).1 hp + mt (Polynomial.map_eq_zero f).1 hp @[simp] theorem degree_map [Semiring S] [Nontrivial S] (p : R[X]) (f : R →+* S) : @@ -494,7 +494,7 @@ theorem rootSet_prod [CommRing S] [IsDomain S] [Algebra R S] {ι : Type*} (f : classical simp only [rootSet, aroots, ← Finset.mem_coe] rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion] - rwa [← Polynomial.map_prod, Ne, map_eq_zero] + rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero] theorem exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, IsRoot p x := ⟨-(p.coeff 0 / p.coeff 1), by @@ -555,10 +555,10 @@ theorem coe_normUnit_of_ne_zero [DecidableEq R] (hp : p ≠ 0) : theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y := by by_cases H : x = 0 - · rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero] + · rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero] · classical rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply, - coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (map_eq_zero f).1 H), + coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H), leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul, map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)] diff --git a/Mathlib/Algebra/Polynomial/Splits.lean b/Mathlib/Algebra/Polynomial/Splits.lean index 49d517483faae..faffbfa26932e 100644 --- a/Mathlib/Algebra/Polynomial/Splits.lean +++ b/Mathlib/Algebra/Polynomial/Splits.lean @@ -263,7 +263,7 @@ variable (i : K →+* L) /-- This lemma is for polynomials over a field. -/ theorem splits_iff (f : K[X]) : Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1 := by - rw [Splits, map_eq_zero] + rw [Splits, Polynomial.map_eq_zero] /-- This lemma is for polynomials over a field. -/ theorem Splits.def {i : K →+* L} {f : K[X]} (h : Splits i f) :