Commit 2026-07-15 01:00 462dde94

View on Github →

chore(RingTheory/IntegralClosure/Algebra/Basic): generalize isIntegral_natCast and isIntegral_intCast (#41746) This PR generalizes isIntegral_natCast and isIntegral_intCast to be over an arbitrary base ring. I also renamed the IsAlgebraic lemmas to match.

Estimated changes

deleted theorem isAlgebraic_int
added theorem isAlgebraic_intCast
deleted theorem isAlgebraic_nat
added theorem isAlgebraic_natCast
deleted theorem isAlgebraic_rat
added theorem isAlgebraic_ratCast
modified theorem isIntegral_intCast
modified theorem isIntegral_natCast