Commit 2024-11-04 14:44 9ddc9e9c

View on Github →

feat(RingTheory/Algebraic[Independent]): some more results on transcendental and algebraically independent (#18433) general properties:

  • make is_transcendental_of_subsingleton a nontriviality lemma
  • IsAlgebraic.[of_]ringHom_of_comp_eq, isAlgebraic_ringHom_iff_of_comp_eq: generalize the similar result for algHom
  • Transcendental.of_tower_top[_of_injective]: negation of IsAlgebraic.tower_top[_of_injective]
  • algebraicIndependent_of_finite_type': Type version of algebraicIndependent_of_finite', which will be used later properties on polynomials:
  • Transcendental.aeval_of_transcendental, Transcendental.of_aeval, transcendental_aeval_iff, IsAlgebraic.of_aeval_of_transcendental: f(r) : A is transcendental over R if and only if r : A and f : R[X] are both transcendental over R
  • move MvPolynomial.transcendental_X to earlier file
  • MvPolynomial.transcendental_supported_polynomial_aeval_X[_iff]: f(X_i) is transcendental over R[X_j | j \in S] if and only if i \notin S and f : R[X] is transcendental over R
  • MvPolynomial.transcendental_polynomial_aeval_X[_iff]: f(X_i) is transcendental over R if and only if f : R[X] is transcendental over R
  • MvPolynomial.transcendental_supported_X[_iff]: X_i is transcendental over R[X_j | j \in S] if and only if i \notin S
  • MvPolynomial.algebraicIndependent_polynomial_aeval_X: f_i(X_i) is algebraically independent over R if each f_i : R[X] is transcendental over R

Estimated changes