Theorem IntermediateField.restrictRestrictAlgEquivMapHom_injective

Modification history

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_injectiveView on Github →