From bb79602cad103fefd1953a2119070cb732e1bd81 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 16:43:02 +0000 Subject: [PATCH] chore(Data/Polynomial/FieldDivision): use `by_cases` instead of `if` This is easier to remove from the `classical` locale in future, and is arguably more readable --- Mathlib/Data/Polynomial/FieldDivision.lean | 48 +++++++++++----------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/Mathlib/Data/Polynomial/FieldDivision.lean b/Mathlib/Data/Polynomial/FieldDivision.lean index 39ec433c3a2e3..ecac3e5dcf7e1 100644 --- a/Mathlib/Data/Polynomial/FieldDivision.lean +++ b/Mathlib/Data/Polynomial/FieldDivision.lean @@ -69,7 +69,7 @@ section NormalizationMonoid variable [NormalizationMonoid R] -instance : NormalizationMonoid R[X] where +instance instNormalizationMonoid : NormalizationMonoid R[X] where normUnit p := ⟨C ↑(normUnit p.leadingCoeff), C ↑(normUnit p.leadingCoeff)⁻¹, by rw [← RingHom.map_mul, Units.mul_inv, C_1], by rw [← RingHom.map_mul, Units.inv_mul, C_1]⟩ @@ -170,10 +170,10 @@ def mod (p q : R[X]) := p %ₘ (q * C (leadingCoeff q)⁻¹) #align polynomial.mod Polynomial.mod -private theorem quotient_mul_add_remainder_eq_aux (p q : R[X]) : q * div p q + mod p q = p := - if h : q = 0 then by simp only [h, MulZeroClass.zero_mul, mod, modByMonic_zero, zero_add] - else by - conv => +private theorem quotient_mul_add_remainder_eq_aux (p q : R[X]) : q * div p q + mod p q = p := by + by_cases h : q = 0 + · simp only [h, zero_mul, mod, modByMonic_zero, zero_add] + · conv => rhs rw [← modByMonic_add_div p (monic_mul_leadingCoeff_inv h)] rw [div, mod, add_comm, mul_assoc] @@ -257,10 +257,10 @@ theorem degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) : rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul] #align polynomial.degree_add_div Polynomial.degree_add_div -theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p := - if hq : q = 0 then by simp [hq] - else by - rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]; exact degree_divByMonic_le _ _ +theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p := by + by_cases hq : q = 0 + · simp [hq] + · rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]; exact degree_divByMonic_le _ _ #align polynomial.degree_div_le Polynomial.degree_div_le theorem degree_div_lt (hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p := by @@ -302,10 +302,10 @@ theorem map_div [Field k] (f : R →+* k) : (p / q).map f = p.map f / q.map f := Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀] #align polynomial.map_div Polynomial.map_div -theorem map_mod [Field k] (f : R →+* k) : (p % q).map f = p.map f % q.map f := - if hq0 : q = 0 then by simp [hq0] - else by - rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f, +theorem map_mod [Field k] (f : R →+* k) : (p % q).map f = p.map f % q.map f := by + by_cases hq0 : q = 0 + · simp [hq0] + · rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f, map_modByMonic f (monic_mul_leadingCoeff_inv hq0)] #align polynomial.map_mod Polynomial.map_mod @@ -450,7 +450,8 @@ theorem dvd_C_mul (ha : a ≠ 0) : p ∣ Polynomial.C a * q ↔ p ∣ q := set_option linter.uppercaseLean3 false in #align polynomial.dvd_C_mul Polynomial.dvd_C_mul -theorem coe_normUnit_of_ne_zero (hp : p ≠ 0) : (normUnit p : R[X]) = C p.leadingCoeff⁻¹ := by +theorem coe_normUnit_of_ne_zero (hp : p ≠ 0) : + (normUnit p : R[X]) = C p.leadingCoeff⁻¹ := by have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp simp [CommGroupWithZero.coe_normUnit _ this] #align polynomial.coe_norm_unit_of_ne_zero Polynomial.coe_normUnit_of_ne_zero @@ -458,9 +459,10 @@ theorem coe_normUnit_of_ne_zero (hp : p ≠ 0) : (normUnit p : R[X]) = C p.leadi theorem normalize_monic (h : Monic p) : normalize p = p := by simp [h] #align polynomial.normalize_monic Polynomial.normalize_monic -theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y := - if H : x = 0 then by rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero] - else by +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] + · 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), leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul, @@ -470,22 +472,22 @@ theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map theorem degree_normalize : degree (normalize p) = degree p := by simp #align polynomial.degree_normalize Polynomial.degree_normalize -theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := +theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := by have : Prime (normalize p) := Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize) (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp)) - (normalize_associated _).prime this + exact (normalize_associated _).prime this #align polynomial.prime_of_degree_eq_one Polynomial.prime_of_degree_eq_one theorem irreducible_of_degree_eq_one (hp1 : degree p = 1) : Irreducible p := (prime_of_degree_eq_one hp1).irreducible #align polynomial.irreducible_of_degree_eq_one Polynomial.irreducible_of_degree_eq_one -theorem not_irreducible_C (x : R) : ¬Irreducible (C x) := - if H : x = 0 then by - rw [H, C_0] +theorem not_irreducible_C (x : R) : ¬Irreducible (C x) := by + by_cases H : x = 0 + · rw [H, C_0] exact not_irreducible_zero - else fun hx => Irreducible.not_unit hx <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H + · exact fun hx => Irreducible.not_unit hx <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H set_option linter.uppercaseLean3 false in #align polynomial.not_irreducible_C Polynomial.not_irreducible_C