English
Under certain conditions, two representations of a polynomial f as an expansion by p^n with g separable and irreducible imply equality of n and g; uniqueness of separable factors of irreducible polynomials is obtained.
Русский
При некоторых условиях два представления f как.expand(p^n, g) с g сепарабельным и неприводимым приводят к равенству n и g; достигается уникальность сепарабельных факторов неприводимых полиномов.
LaTeX
$$$\\text{If } f \\text{ irreducible and } f = \\text{expand}(p^n, g) \\text{ with } g \\text{ Separable}, \\text{ then } n \\,=\, n' \\text{ and } g \\,=\\, g'.$$$
Lean4
theorem unique_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ : ℕ) (g₁ : F[X])
(hg₁ : g₁.Separable) (hgf₁ : expand F (p ^ n₁) g₁ = f) (n₂ : ℕ) (g₂ : F[X]) (hg₂ : g₂.Separable)
(hgf₂ : expand F (p ^ n₂) g₂ = f) : n₁ = n₂ ∧ g₁ = g₂ :=
by
revert g₁ g₂
wlog hn : n₁ ≤ n₂
· intro g₁ hg₁ Hg₁ g₂ hg₂ Hg₂
simpa only [eq_comm] using this p hf hp n₂ n₁ (le_of_not_ge hn) g₂ hg₂ Hg₂ g₁ hg₁ Hg₁
intro g₁ hg₁ hgf₁ g₂ hg₂ hgf₂
rw [le_iff_exists_add] at hn
rcases hn with ⟨k, rfl⟩
rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂
subst hgf₂
subst hgf₁
rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)
· rw [isUnit_iff] at h
rcases h with ⟨r, hr, rfl⟩
simp_rw [expand_C] at hf
exact absurd (isUnit_C.2 hr) hf.1
· rw [add_zero, pow_zero, expand_one]
constructor <;> rfl
