Commit 2026-04-15 19:09 2a556ee3

View on Github →

feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421) Alternative hypothesis to existing theorem: prove the result from a Module.Free hypothesis instead of IsIntegrallyClosed. If α generates S as an algebra, then S is given by adjoining a root of minpoly R α.

Estimated changes

Modified Mathlib/Analysis/Complex/Polynomial/Basic.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

deleted theorem minpoly.degree_le

deleted theorem minpoly.natDegree_le

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Exponent.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

added theorem Algebra.aeval_self_charpoly_lmul

modified theorem LinearMap.charpoly_natDegree

added theorem minpoly.degree_le

added theorem minpoly.natDegree_le

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem LinearMap.finrank_le_finrank_of_surjective

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

added def IsAdjoinRootMonic.mkOfAdjoinEqTop'

added theorem IsAdjoinRootMonic.mkOfAdjoinEqTop'_root

Modified Mathlib/RingTheory/OrzechProperty.lean

added theorem OrzechProperty.bijective_of_surjective_of_injective

Modified Mathlib/RingTheory/Valuation/Minpoly.lean