Commit 2023-09-11 15:07 23cd2eab

View on Github →

chore: reduce imports to Data/Nat/Cast/Basic and Data/Rat/Defs (#7093)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

deleted theorem Commute.ofNat_left

deleted theorem Commute.ofNat_right

deleted theorem Nat.abs_cast

deleted def Nat.castOrderEmbedding

deleted theorem Nat.cast_comm

deleted theorem Nat.cast_commute

deleted theorem Nat.cast_le

deleted theorem Nat.cast_le_one

deleted theorem Nat.cast_lt

deleted theorem Nat.cast_lt_one

deleted theorem Nat.commute_cast

deleted theorem Nat.one_le_cast

deleted theorem Nat.one_lt_cast

deleted theorem Nat.strictMono_cast

deleted theorem NeZero.nat_of_injective

Created Mathlib/Data/Nat/Cast/Commute.lean

added theorem Commute.ofNat_left

added theorem Commute.ofNat_right

added theorem Nat.cast_comm

added theorem Nat.cast_commute

added theorem Nat.commute_cast

Modified Mathlib/Data/Nat/Cast/Field.lean

Created Mathlib/Data/Nat/Cast/Order.lean

added theorem Nat.abs_cast

added def Nat.castOrderEmbedding

added theorem Nat.cast_le

added theorem Nat.cast_le_one

added theorem Nat.cast_lt

added theorem Nat.cast_lt_one

added theorem Nat.one_le_cast

added theorem Nat.one_lt_cast

added theorem Nat.strictMono_cast

added theorem NeZero.nat_of_injective

Modified Mathlib/Data/Nat/Choose/Central.lean

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/Data/Rat/Lemmas.lean