Theorem IntermediateField.extendRight.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.extendRight.coe_extendRightEquiv'View on Github →