comap_ne_bot_of_integral_mem — Mathlib

English

If x is nonzero, x ∈ I, and hx is integral, then the comap is nonzero.

Русский

Если x ≠ 0 и x ∈ I и hx целевая интегральная, тогда обратный образ не равен нулю.

LaTeX

$$$$\text{If } x \neq 0,\ x \in I,\ IsIntegral R x \Rightarrow I^{\mathrm{comap}} \neq \bot.$$$$

Lean4

theorem comap_ne_bot_of_integral_mem [Nontrivial R] [IsDomain S] {x : S} (x_ne_zero : x ≠ 0) (x_mem : x ∈ I)
    (hx : IsIntegral R x) : I.comap (algebraMap R S) ≠ ⊥ :=
  comap_ne_bot_of_algebraic_mem x_ne_zero x_mem hx.isAlgebraic

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