mem_adjoin_iff_div — Mathlib

English

An element x lies in adjoin F S if and only if it can be written as a quotient of two elements from Algebra.adjoin F S.

Русский

Элемент x принадлежит adjoin F S тогда и только тогда, когда его можно записать как отношение двух элементов из Algebra.adjoin F S.

LaTeX

$$x \in \operatorname{adjoin}_F S \iff \exists r \in \operatorname{Algebra.adjoin}_F S, \exists s \in \operatorname{Algebra.adjoin}_F S, x = r / s$$

Lean4

theorem mem_adjoin_iff_div {x : E} : x ∈ adjoin F S ↔ ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s :=
  by
  simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring, Subfield.mem_closure_iff, ←
    Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_comm]

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