Commit 2025-08-18 12:21 44799e11

View on Github →

feat(RingTheory/IsAdjoinRoot): add properties and constructors (#27373)

Add facts about IsAdjoinRoot: root is primitive, root is algebraic/integral, extension dimension, isomorphism with AdjoinRoot
- Redefine isomorphism constructors to use the isomorphism with AdjoinRoot
Add constructors for IsAdjoinRoot from primitive element

Estimated changes

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

added theorem Algebra.adjoin_eq_top_of_intermediateField

added theorem Algebra.adjoin_eq_top_of_primitive_element

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

added def IsAdjoinRoot.adjoinRootAlgEquiv

added theorem IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map

added theorem IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk

added theorem IsAdjoinRoot.adjoinRootAlgEquiv_apply_root

added theorem IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk

added theorem IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root

added theorem IsAdjoinRoot.adjoin_root_eq_top

modified def IsAdjoinRoot.algEquiv

modified theorem IsAdjoinRoot.algEquiv_algEquiv

added theorem IsAdjoinRoot.algEquiv_apply_map

added theorem IsAdjoinRoot.algEquiv_def

modified theorem IsAdjoinRoot.algEquiv_map

modified theorem IsAdjoinRoot.algEquiv_ofAlgEquiv

modified theorem IsAdjoinRoot.algEquiv_root

modified theorem IsAdjoinRoot.algEquiv_self

modified theorem IsAdjoinRoot.algEquiv_symm

modified theorem IsAdjoinRoot.algEquiv_trans

added theorem IsAdjoinRoot.isAlgebraic_root

modified theorem IsAdjoinRoot.liftHom_algEquiv

modified theorem IsAdjoinRoot.lift_algEquiv

added def IsAdjoinRoot.mkOfAdjoinEqTop

added theorem IsAdjoinRoot.mkOfAdjoinEqTop_root

modified theorem IsAdjoinRoot.ofAlgEquiv_algEquiv

modified theorem IsAdjoinRoot.ofAlgEquiv_root

added theorem IsAdjoinRoot.primitive_element_root

added theorem IsAdjoinRootMonic.finite

added theorem IsAdjoinRootMonic.finrank