Theorem IntermediateField.algebraMap_extendRightEquiv_symm

Modification history

2026-04-13 15:12
Mathlib/FieldTheory/IntermediateField/ExtendRight.lean
feat(FieldTheory/IntermediateField): define the image of an intermediate field in a larger extension (#36772) …
Added IntermediateField.algebraMap_extendRightEquiv_symmView on Github →