From b1556bbbbd8d64d5c27db7c0440ee7239f8ecf46 Mon Sep 17 00:00:00 2001 From: Jz Pan Date: Mon, 25 Dec 2023 18:05:55 +0000 Subject: [PATCH] feat(Data/Polynomial/Expand): add `leadingCoeff_expand` and `monic_expand_iff` (#9261) The first states that `expand` preserves leading coefficient; the second states that `expand` preserves monicity, hence gives a converse to `Monic.expand`. --- Mathlib/Data/Polynomial/Expand.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Polynomial/Expand.lean b/Mathlib/Data/Polynomial/Expand.lean index e49abfdba91c5..795deb2c365bc 100644 --- a/Mathlib/Data/Polynomial/Expand.lean +++ b/Mathlib/Data/Polynomial/Expand.lean @@ -170,9 +170,14 @@ theorem natDegree_expand (p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.nat exact mt leadingCoeff_eq_zero.1 hf #align polynomial.nat_degree_expand Polynomial.natDegree_expand -theorem Monic.expand {p : ℕ} {f : R[X]} (hp : 0 < p) (h : f.Monic) : (expand R p f).Monic := by - rw [Monic.def, Polynomial.leadingCoeff, natDegree_expand, coeff_expand hp] - simp [hp, h] +theorem leadingCoeff_expand {p : ℕ} {f : R[X]} (hp : 0 < p) : + (expand R p f).leadingCoeff = f.leadingCoeff := by + simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp] + +theorem monic_expand_iff {p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).Monic ↔ f.Monic := by + simp only [Monic, leadingCoeff_expand hp] + +alias ⟨_, Monic.expand⟩ := monic_expand_iff #align polynomial.monic.expand Polynomial.Monic.expand theorem map_expand {p : ℕ} {f : R →+* S} {q : R[X]} :