transcendental_iff_ker_eq_bot — Mathlib

English

An element x is transcendental over R iff the kernel of the ring homomorphism aeval x is the zero ideal.

Русский

Элемент x трансцендентен над R тогда и только тогда, когда ядро гомоморфизма aeval x равно нулевому идеалу.

LaTeX

$$$ Transcendental R x \iff \ RingHom.ker (aeval (R := R) x) = \bot $$$

Lean4

/-- An element `x` is transcendental over `R` if and only if the kernel of the ring homomorphism
`Polynomial.aeval x` is the zero ideal. This is similar to `algebraicIndependent_iff_ker_eq_bot`. -/
theorem transcendental_iff_ker_eq_bot {x : A} : Transcendental R x ↔ RingHom.ker (aeval (R := R) x) = ⊥ := by
  rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]

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