Commit 2023-11-16 13:41 a76dc22f

View on Github →

chore(RingTheory/{Algebraic, Localization/Integral}): rename decls to use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by this Zulip thread, I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |

Estimated changes

added theorem IsAlgebraic.of_finite
added theorem IsAlgebraic.of_pow
deleted theorem isAlgebraic_of_finite
deleted theorem isAlgebraic_of_pow
deleted theorem FG_adjoin_of_finite
added theorem IsIntegral.add
deleted theorem IsIntegral.algebraMap
added theorem IsIntegral.map
added theorem IsIntegral.mul
added theorem IsIntegral.neg
added theorem IsIntegral.of_finite
added theorem IsIntegral.of_mul_unit
added theorem IsIntegral.of_pow
added theorem IsIntegral.of_subring
added theorem IsIntegral.smul
added theorem IsIntegral.sub
added theorem IsIntegral.tower_bot
added theorem fg_adjoin_of_finite
deleted theorem isIntegral_add
deleted theorem isIntegral_mul
deleted theorem isIntegral_neg
deleted theorem isIntegral_ofSubring
deleted theorem isIntegral_of_finite
deleted theorem isIntegral_of_mem_closure
deleted theorem isIntegral_of_mem_of_FG
deleted theorem isIntegral_of_pow
deleted theorem isIntegral_smul
deleted theorem isIntegral_sub
deleted theorem map_isIntegral