map_denom_ne_zero — Mathlib

English

Let φ be a map from K[X] into some L with φ injective on nonzero divisors; for any RatFunc f, φ(denom f) ≠ 0.

Русский

Пусть φ — отображение из K[X] в L с инъективностью на множителях без нулевых делителей; для любой RatFunc f верно φ(denom f) ≠ 0.

LaTeX

$$$\\forall f,\\; φ(\\denom(f)) \\neq 0$$$

Lean4

theorem map_denom_ne_zero {L F : Type*} [Zero L] [FunLike F K[X] L] [ZeroHomClass F K[X] L] (φ : F)
    (hφ : Function.Injective φ) (f : RatFunc K) : φ f.denom ≠ 0 := fun H =>
  (denom_ne_zero f) ((map_eq_zero_iff φ hφ).mp H)

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