Commit 2024-08-29 12:34 cc59ee86

View on Github →

chore: move some IsIntegral results earlier (#16229) The first section of Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic contained results that could just as easily go into earlier files.

Estimated changes

added theorem IsIntegral.of_subring
added theorem IsIntegral.tower_top
added theorem fg_adjoin_of_finite
added theorem isIntegral_algEquiv
added theorem map_isIntegral_int
deleted theorem IsIntegral.map_of_comp_eq
deleted theorem IsIntegral.of_subring
deleted theorem IsIntegral.tower_top
deleted theorem fg_adjoin_of_finite
deleted theorem isIntegral_algEquiv
deleted theorem isIntegral_algebraMap_iff
deleted theorem isIntegral_of_noetherian
deleted theorem map_isIntegral_int