Commit 2024-07-03 02:04 e66c5a96

View on Github →

chore (Data.Nat.Cast.Order): split into Basic and Ring (#14371) We split Data.Nat.Cast.Order into Data.Nat.Cast.Order.Basic which only uses unbundled ordered algebra classes and Data.Nat.Cast.Order.Ring which uses bundled ordered algebra classes. This avoids importing bundled ordered algebra until later downstream.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group/Nat.lean

deleted theorem NeZero.one_le

Modified Mathlib/Algebra/Order/Invertible.lean

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

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

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

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

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

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

added theorem NeZero.one_le

Renamed Mathlib/Data/Nat/Cast/Order.lean to Mathlib/Data/Nat/Cast/Order/Basic.lean

deleted theorem Nat.abs_cast

deleted theorem Nat.abs_ofNat

deleted theorem Nat.cast_max

deleted theorem Nat.cast_min

deleted theorem Nat.cast_nonneg

deleted theorem Nat.cast_pos

deleted theorem Nat.cast_tsub

deleted theorem Nat.ofNat_nonneg

deleted theorem Nat.ofNat_pos'

deleted theorem Nat.ofNat_pos

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

added theorem Nat.abs_cast

added theorem Nat.abs_ofNat

added theorem Nat.cast_max

added theorem Nat.cast_min

added theorem Nat.cast_nonneg

added theorem Nat.cast_pos

added theorem Nat.cast_tsub

added theorem Nat.ofNat_nonneg

added theorem Nat.ofNat_pos'

added theorem Nat.ofNat_pos

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

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

Modified Mathlib/ModelTheory/Algebra/Field/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean