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.

Estimated changes