Commit 2025-11-08 12:17 e2aa38b8

View on Github →

chore(Algebra/Order/Ring): deprecate Int.cast_natAbs (#28384)

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Cast.lean

deleted theorem Int.cast_natAbs

Modified Mathlib/Data/NNReal/Defs.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/RingTheory/FractionalIdeal/Norm.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean