Commit 2025-09-01 08:25 a52ec4ba

View on Github →

refactor: generalize galRestrict to different rings (#28847) This adds a new galRestrict' which generalizes the forward direction of galRestrict, and genrealizes galLift in-place.

Estimated changes

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

added theorem algebraMap_galRestrict'_apply

modified def galLift

added theorem galLift_algebraMap_apply

added theorem galLift_comp

added theorem galLift_galRestrict'

added def galRestrict'

added theorem galRestrict'_comp

added theorem galRestrict'_galLift