mem_range_of_degree_eq_one — Mathlib

English

If B is a subsingleton, then minpoly_A(x) = 1.

Русский

Если B является подсобыдной областью, то minpoly_A(x) = 1.

LaTeX

$$$\\minpoly_A(x) = 1.$$$

Lean4

theorem mem_range_of_degree_eq_one (hx : (minpoly A x).degree = 1) : x ∈ (algebraMap A B).range :=
  by
  have h : IsIntegral A x := by
    by_contra h
    rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
    exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
  have key := minpoly.aeval A x
  rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add, aeval_C, aeval_X, ←
    eq_neg_iff_add_eq_zero, ← RingHom.map_neg] at key
  exact ⟨-(minpoly A x).coeff 0, key.symm⟩

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