English
For p, q ∈ R[X], the degree of the norm of p·1 + q·Y equals max(2 deg p, 2 deg q + 3).
Русский
Для p, q ∈ R[X] степень нормы элемента p·1 + q·Y равна max(2·deg p, 2·deg q + 3).
LaTeX
$$$\\deg\\big(\\operatorname{norm}_{R[X]}(p\\cdot 1 + q\\cdot Y)\\big) = \\max\\big(2\\,\\deg p,\\; 2\\,\\deg q + 3\\big)$$$
Lean4
theorem degree_norm_smul_basis [IsDomain R] (p q : R[X]) :
(Algebra.norm R[X] <| p • 1 + q • mk W' Y).degree = max (2 • p.degree) (2 • q.degree + 3) :=
by
have hdp : (p ^ 2).degree = 2 • p.degree := degree_pow p 2
have hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1 := by
simpa only [degree_mul] using add_le_add_left degree_linear_le (p.degree + q.degree)
have hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3 := by
rw [degree_mul, degree_pow, ← one_mul <| X ^ 3, ← C_1, degree_cubic <| one_ne_zero' R]
rw [norm_smul_basis]
by_cases hp : p = 0
· simp only [hp, hdq, neg_zero, zero_sub, zero_mul, zero_pow two_ne_zero, degree_neg]
exact (max_bot_left _).symm
· by_cases hq : q = 0
· simp only [hq, hdp, sub_zero, zero_mul, mul_zero, zero_pow two_ne_zero]
exact (max_bot_right _).symm
· rw [← not_congr degree_eq_bot] at hp hq
rcases hp' : p.degree with _ | dp
· exact (hp hp').elim
· rw [hp'] at hdp hdpq
rcases hq' : q.degree with _ | dq
· exact (hq hq').elim
· rw [hq'] at hdpq hdq
rcases le_or_gt dp (dq + 1) with hpq | hpq
·
convert
(degree_sub_eq_right_of_degree_lt <|
(degree_sub_le _ _).trans_lt <| max_lt_iff.mpr ⟨hdp.trans_lt _, hdpq.trans_lt _⟩).trans
(max_eq_right_of_lt _).symm <;>
rw [hdq] <;>
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]
· rw [sub_sub]
convert
(degree_sub_eq_left_of_degree_lt <|
(degree_add_le _ _).trans_lt <| max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
(max_eq_left_of_lt _).symm <;>
rw [hdp] <;>
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]
