Commit 2023-12-18 13:47 9e1e18da

View on Github →

feat: Restriction of galois group onto integrally closed subrings. (#9113)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

modified theorem IsIntegralClosure.isLocalization

added theorem IsIntegralClosure.isLocalization_of_isSeparable

Created Mathlib/RingTheory/IntegralRestrict.lean

added theorem algebraMap_galRestrictHom_apply

added theorem algebraMap_galRestrict_apply

added theorem coe_galRestrict_apply

added def galLift

added def galRestrict

added def galRestrictHom

added theorem galRestrictHom_symm_algebraMap_apply

added theorem galRestrict_apply

added theorem prod_galRestrict_eq_norm