English
For monic p and p ≠ 1, Irreducible p iff for all monic q with natDegree q ∈ Ioc 0 (natDegree p / 2), q ∤ p.
Русский
Для моноического p и p ≠ 1 irreducible p тогда и только тогда, когда для каждого моноичного q со степенью natDegree q ∈ Ioc 0 (natDegree p / 2) не выполняется q | p.
LaTeX
$$$Monic(p) \land p \neq 1 \Rightarrow (Irreducible(p) \iff \forall q, Monic(q) \rightarrow natDegree(q) \in Finset.Ioc 0 (natDegree(p) / 2) \rightarrow q \nmid p)$$$
Lean4
theorem not_irreducible_iff_exists_add_mul_eq_coeff (hm : p.Monic) (hnd : p.natDegree = 2) :
¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂ :=
by
cases subsingleton_or_nontrivial R
· simp [natDegree_of_subsingleton] at hnd
rw [hm.irreducible_iff_natDegree', and_iff_right, hnd]
· push_neg
constructor
· rintro ⟨a, b, ha, hb, rfl, hdb⟩
simp only [zero_lt_two, Nat.div_self, Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb
have hda := hnd
rw [ha.natDegree_mul hb, hdb] at hda
use a.coeff 0, b.coeff 0, mul_coeff_zero a b
simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using ha.nextCoeff_mul hb
· rintro ⟨c₁, c₂, hmul, hadd⟩
refine ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
· rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_one, ← hnd,
hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
ring
· simp
· rintro rfl
simp [natDegree_one] at hnd
