English
If s,t are subsets with s being a basis of t in the matroid of A over R, then every element a of A is algebraic over the subalgebra adjoin_R s if and only if it is algebraic over adjoin_R t.
Русский
Пусть s,t — подмножества такие, что s образует базис t в матроиде A над R; тогда для любого элемента a ∈ A тождественно выполняется: a алгебраичен над подалгеброй adjoin_R s тогда и только что над adjoin_R t.
LaTeX
$$$ ( \\mathrm{matroid} \\, R\\, A ).IsBasis(s,t) \\Rightarrow \\forall a \\in A,\\; IsAlgebraic(\\operatorname{adjoin}_R s)\, a \\iff IsAlgebraic(\\operatorname{adjoin}_R t)\\, a $$$
Lean4
theorem isAlgebraic_adjoin_iff_of_matroid_isBasis [NoZeroDivisors A] {s t : Set A} {a : A}
(h : (matroid R A).IsBasis s t) : IsAlgebraic (adjoin R s) a ↔ IsAlgebraic (adjoin R t) a :=
by
cases subsingleton_or_nontrivial A
· apply iff_of_false <;> apply is_transcendental_of_subsingleton
have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
exact
⟨(·.adjoin_of_forall_isAlgebraic fun x hx ↦ (hx.2 <| h.1.1.2 hx.1).elim),
(·.adjoin_of_forall_isAlgebraic fun x hx ↦ (matroid_isBasis_iff.mp h).2.2 _ hx.1)⟩
