English
If ι has a unique element, then AlgebraicIndependent R x is equivalent to Transcendental R (x at the unique index).
Русский
Если множество индексов имеет ровно один элемент, то AlgebraicIndependent R x эквивалентно Transcendental R (x на единственном индексе).
LaTeX
$$$\forall \{\iota\} \, \text{Unique } \iota:\ AlgebraicIndependent R x \leftrightarrow Transcendental R (x\,\text{default})$$$
Lean4
/-- A one-element family `x` is algebraically independent if and only if
its element is transcendental. -/
@[simp]
theorem algebraicIndependent_unique_type_iff [Unique ι] : AlgebraicIndependent R x ↔ Transcendental R (x default) :=
by
rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]
let i := (renameEquiv R (Equiv.equivPUnit.{_, 1} ι)).trans (pUnitAlgEquiv R)
have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i :=
by
ext y
simp [i, Subsingleton.elim y default]
simp [key]
