Theorem IntermediateField.coe_extendRightEquiv

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.coe_extendRightEquivView on Github →