iff_transcendental_adjoin_image — Mathlib

English

Another variant of the finite-type criterion with a specified injective algebra map, transferring finite-subset independence to the whole set.

Русский

Еще одна вариация критерия по конечному множеству с указанной инъекцией алгебраической карты переносит независимость конечного множества на всё множество.

LaTeX

$$$Function.Injective (algebraMap R A) \to ( \forall t, t.Finite \to AlgebraicIndependent R ((\uparrow) : t → A) \to \forall a ∈ s, a ∉ t → Transcendental (adjoin R t) a) \to AlgebraicIndependent R ((\uparrow) : s → A)$$

Lean4

theorem iff_transcendental_adjoin_image (i : ι) :
    AlgebraicIndependent R x ↔
      AlgebraicIndependent R (fun j : { j // j ≠ i } ↦ x j) ∧ Transcendental (adjoin R (x '' { i }ᶜ)) (x i) :=
  (iff_adjoin_image_compl _).trans <| and_congr_right fun _ ↦ algebraicIndependent_unique_type_iff (ι := { j // j = i })

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