Commit 2026-06-03 10:01 2742bd88

View on Github →

feat(RingTheory/IntegralClosure): add IsIntegral helpers for casts (#39873) Add IsIntegral.Cast and IsIntegral.Nat, stating that integer and natural literals are integral over ℤ in a field.

Estimated changes

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

added theorem isIntegral_intCast

added theorem isIntegral_natCast