Theorem isIntegral_natCast

Modification history

2026-07-15 01:00

Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

chore(RingTheory/IntegralClosure/Algebra/Basic): generalize `isIntegral_natCast` and `isIntegral_intCast` (#41746) …

Modified isIntegral_natCast View on Github →

2026-06-03 10:01

Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

feat(RingTheory/IntegralClosure): add IsIntegral helpers for casts (#39873) …

Added isIntegral_natCast View on Github →