Theorem Algebra.adjoin_eq_top_of_primitive_element

Modification history

2025-08-18 12:21

Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

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

Added Algebra.adjoin_eq_top_of_primitive_element View on Github →