Theorem IsScalarTower.AlgEquiv.restrictNormalHom_comp

Modification history

2025-01-23 18:20
Mathlib/FieldTheory/Normal/Basic.lean
refactor(FieldTheory/Normal): Split file (#20724) …
Modified IsScalarTower.AlgEquiv.restrictNormalHom_compView on Github →
2024-10-18 17:54
Mathlib/FieldTheory/Normal.lean
feat(FieldTheory/Galois): Finite galois subextensions (#16978) …
Added IsScalarTower.AlgEquiv.restrictNormalHom_compView on Github →