Commit 2025-12-05 11:03 1097e18b

View on Github →

feat(FieldTheory): fg extension over perfect field is separably generated (#30998)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Perfect.lean

added theorem frobeniusEquiv_symm_pow

Created Mathlib/FieldTheory/SeparablyGenerated.lean

added theorem MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero

added theorem MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_zero

added theorem MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le

added theorem MvPolynomial.irreducible_of_forall_totalDegree_le

added theorem MvPolynomial.irreducible_toPolynomialAdjoinImageCompl

added theorem MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le

added def MvPolynomial.toPolynomialAdjoinImageCompl

added theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'

added theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow

added theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top

added theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fg

added theorem exists_isTranscendenceBasis_and_isSeparable_of_perfectField

Modified Mathlib/RingTheory/AlgebraicIndependent/Defs.lean

added def AlgebraicIndepOn.aevalEquiv

added theorem AlgebraicIndepOn.univ