Commit 2026-06-16 16:57 483ba09b

View on Github →

chore: deprecate Rat.coe_int_inj (#40670)

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Data/Rat/Defs.lean

deleted theorem Rat.coe_int_inj

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean