Commit 2023-09-11 03:33 271b84c0

View on Github →

chore: cleanup imports of Data/Rat/Cast/Defs (#7092) Removing further unnecessary imports on the path to major tactics.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

deleted theorem Rat.cast_inv_int

deleted theorem Rat.cast_inv_nat

Created Mathlib/Data/Rat/Cast/Lemmas.lean

added theorem Rat.cast_inv_int

added theorem Rat.cast_inv_nat

Modified Mathlib/Tactic/NormNum/Inv.lean