English
For polynomials f,g, equality (f g).natSepDegree = f.natSepDegree + g.natSepDegree holds exactly when either f=g=0 or f and g are coprime.
Русский
Справедливо равенство (f g).natSepDegree = f.natSepDegree + g.natSepDegree тогда и только тогда, когда f=g=0 либо f и g взаимно просты.
LaTeX
$$$ (f \cdot g).natSepDegree = f.\natSepDegree + g.\natSepDegree \iff (f = 0 \wedge g = 0) \lor IsCoprime f g $$$
Lean4
theorem natSepDegree_mul_eq_iff (g : F[X]) :
(f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ (f = 0 ∧ g = 0) ∨ IsCoprime f g :=
by
by_cases h : f * g = 0
· rw [mul_eq_zero] at h
wlog hf : f = 0 generalizing f g
· simpa only [mul_comm, add_comm, and_comm, isCoprime_comm] using this g f h.symm (h.resolve_left hf)
rw [hf, zero_mul, natSepDegree_zero, zero_add, isCoprime_zero_left, isUnit_iff, eq_comm, natSepDegree_eq_zero_iff,
natDegree_eq_zero]
refine ⟨fun ⟨x, h⟩ ↦ ?_, ?_⟩
· by_cases hx : x = 0
· exact .inl ⟨rfl, by rw [← h, hx, map_zero]⟩
exact .inr ⟨x, Ne.isUnit hx, h⟩
rintro (⟨-, h⟩ | ⟨x, -, h⟩)
· exact ⟨0, by rw [h, map_zero]⟩
exact ⟨x, h⟩
classical
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
rw [mul_eq_zero, not_or] at h
refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2) fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
· obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
exact
H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩ x
⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
rintro (⟨rfl, rfl⟩ | hc)
· exact (h.1 rfl).elim
rintro x hf _ hg rfl
obtain ⟨u, v, hfg⟩ := hc
simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero, zero_ne_one] using congr(aeval x $hfg)
