mem_adjoin_simple_iff — Mathlib

English

For a singleton set {α}, mem_adjoin_simple_iff gives a concrete description of membership using polynomials in α.

Русский

Для единичного множества {α} даётся конкретное описание принадлежности через полиномы в α.

LaTeX

$$$x \in \operatorname{adjoin}_F \{\alpha\} \\iff \exists r,s : F[X], x = aeval(\alpha) r / aeval(\alpha) s$$$

Lean4

theorem mem_adjoin_simple_iff {α : E} (x : E) : x ∈ adjoin F { α } ↔ ∃ r s : F[X], x = aeval α r / aeval α s := by
  simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]

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