mem_adjoin_iff — Mathlib

English

An element lies in adjoin F S precisely when it can be expressed as a ratio of F-linear combinations of S.

Русский

Элемент принадлежит адъюнкту F S тогда и только тогда, когда его можно выразить как отношение двух элементов, порожденных S над F.

LaTeX

$$$x \in \operatorname{adjoin}_F S \iff \exists r,s : MvPolynomial S F, x = MvPolynomial.aeval Subtype.val r / MvPolynomial.aeval Subtype.val s$$$

Lean4

theorem mem_adjoin_iff (x : E) :
    x ∈ adjoin F S ↔
      ∃ r s : MvPolynomial S F, x = MvPolynomial.aeval Subtype.val r / MvPolynomial.aeval Subtype.val s :=
  by rw [← mem_adjoin_range_iff, Subtype.range_coe]

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