# Commit 2024-10-30 05:09 ef29c80a

View on Github →feat(RingTheory/AlgebraicIndependent): add some results on `AlgebraicIndependent`

(#18378)

`algebraicIndependent_unique_type_iff`

,`algebraicIndependent_iff_transcendental`

: equivalency of`AlgebraicIndependent`

and`Transcendental`

for one-element family`AlgebraicIndependent.transcendental`

: f a family`x`

is algebraically independent, then any of its element is transcendental`MvPolynomial.(algebraicIndependent|transcendental)_X`

: algebraic independent properties of intermediates of`MvPolynomial`

`algebraicIndependent_of_finite'`

: variant of`algebraicIndependent_of_finite`

using`Transcendental`

`exists_isTranscendenceBasis'`

:`Type`

version of`exists_isTranscendenceBasis`

Also changed one`¬IsAlgebraic`

to`Transcendental`

. Also add`Set.subtypeInsertEquivOption`

(used in the proof of`algebraicIndependent_of_finite'`

) which is similar to`Finset.subtypeInsertEquivOption`

. Note that it does not have simp lemmas yet, as the existing`Finset`

one has no simp lemmas, either.