X_pow_mul_sub_C_irreducible — Mathlib

English

If L/K is finite dimensional, the Krull topology on Aut_K(L) is discrete.

Русский

Если размерность L над K конечна, то топология Круль на Aut_K(L) дискретна.

LaTeX

$$$\\text{DiscreteTopology}(\\mathrm{AlgEquiv}(K,L,L)).$$$

Lean4

theorem X_pow_mul_sub_C_irreducible {n m : ℕ} {a : K} (hm : Irreducible (X ^ m - C a))
    (hn :
      ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (_ : minpoly K x = X ^ m - C a),
        Irreducible (X ^ n - C (AdjoinSimple.gen K x))) :
    Irreducible (X ^ (n * m) - C a) :=
  by
  have hm' : m ≠ 0 := by
    rintro rfl
    rw [pow_zero, ← C.map_one, ← map_sub] at hm
    exact not_irreducible_C _ hm
  simpa [pow_mul] using
    irreducible_comp (monic_X_pow_sub_C a hm') (monic_X_pow n) hm
      (by simpa only [Polynomial.map_pow, map_X] using hn)
        -- TODO: generalize to even `n`

Похожие утверждения