Commit 2023-07-27 01:08 c954df28

View on Github →

chore(FieldTheory/Adjoin): remove unnecessary assumptions in minpolynatDegree_le and minpoly.degree_le (#6152) Also

  • fix the names of minpoly.natDegree_le and minpoly.degree_le
  • rename minpoly.ne_zero_of_finite_field_extension to minpoly.ne_zero_of_finite
  • reduce typeclass assumptions of some lemmas in RingTheory/Algebraic
  • add two lemmas isIntegral_of_finite and isAlgebraic_of_finite
  • move Algebra.isIntegral_of_finite to RingTheory/IntegralClosure

Estimated changes

added theorem minpoly.degree_le
added theorem minpoly.natDegree_le
modified theorem AlgHom.bijective
modified theorem Algebra.isAlgebraic_trans
added theorem isAlgebraic_of_finite
modified theorem isAlgebraic_of_larger_base
added theorem isIntegral_of_finite