comap_ne_bot_of_algebraic_mem — Mathlib

English

If x ≠ 0 is algebraic over R in S, then the comap of I is not the bottom ideal.

Русский

Если x ≠ 0 и алгебраически зависим над R в S, то образ обратного образа идеала не равен нулю.

LaTeX

$$$$I^{\mathrm{comap} f} \neq \bot.$$$$

Lean4

theorem comap_ne_bot_of_algebraic_mem [IsDomain S] {x : S} (x_ne_zero : x ≠ 0) (x_mem : x ∈ I) (hx : IsAlgebraic R x) :
    I.comap (algebraMap R S) ≠ ⊥ :=
  let ⟨_, p_ne_zero, hp⟩ := hx
  comap_ne_bot_of_root_mem x_ne_zero x_mem p_ne_zero hp

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