Theorem IntermediateField.restrictRestrictAlgEquivMapHom_apply

Modification history

2025-10-16 07:33
Mathlib/FieldTheory/Galois/Basic.lean
feat: notation for galois group (#30266) …
Modified IntermediateField.restrictRestrictAlgEquivMapHom_applyView on Github →
2025-09-26 08:53
Mathlib/FieldTheory/Galois/Basic.lean
feat(FieldTheory/IsGalois): map induced by the restriction to a subfield (#26841) …
Added IntermediateField.restrictRestrictAlgEquivMapHom_applyView on Github →