Commit 2025-07-06 08:48 2c5d23c6

View on Github →

feat(RingTheory): degree of rational function field extension (#26316) This PR continues the work from #22966. Original PR: https://github.com/leanprover-community/mathlib4/pull/22966

Estimated changes

Modified Mathlib/RingTheory/AdjoinRoot.lean

deleted theorem Polynomial.exists_dvd_map_of_isAlgebraic

Modified Mathlib/RingTheory/Algebraic/Basic.lean

modified theorem IsAlgebraic.exists_nonzero_dvd

modified theorem IsAlgebraic.exists_nonzero_eq_adjoin_mul

modified theorem Subalgebra.inv_mem_of_algebraic

modified theorem Subalgebra.isAlgebraic_of_isAlgebraic_bot

Modified Mathlib/RingTheory/Algebraic/Integral.lean

added theorem Algebra.IsAlgebraic.finrank_of_isFractionRing

added theorem Algebra.IsAlgebraic.isBaseChange_of_isFractionRing

added theorem Algebra.IsAlgebraic.lift_rank_of_isFractionRing

added theorem Algebra.IsAlgebraic.rank_fractionRing

added theorem Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial

added theorem Algebra.IsAlgebraic.rank_fractionRing_polynomial

added theorem Algebra.IsAlgebraic.rank_of_isFractionRing

added theorem Algebra.IsPushout.isAlgebraic'

added theorem Algebra.IsPushout.isAlgebraic

added theorem IsAlgebraic.tmul

added theorem MvPolynomial.exists_dvd_map_of_isAlgebraic

added theorem Polynomial.exists_dvd_map_of_isAlgebraic

added theorem rank_mvPolynomial_mvPolynomial

added theorem rank_polynomial_polynomial

Modified Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

added theorem Algebra.IsPushout.isIntegral'

added theorem Algebra.IsPushout.isIntegral

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.right_algebraMap_apply