Commit 2023-09-06 22:20 8f46576d

View on Github →

chore: cleanup in Mathlib.Init (#6977)

Estimated changes

Modified Archive/Arithcc.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/CharZero/Defs.lean

Modified Mathlib/Algebra/Field/Defs.lean

Modified Mathlib/Algebra/Field/IsField.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/NeZero.lean

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Control/Random.lean

Modified Mathlib/Data/Char.lean

Modified Mathlib/Data/FunLike/Basic.lean

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

Modified Mathlib/Data/Nat/Basic.lean

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

Modified Mathlib/Data/Option/Basic.lean

Modified Mathlib/Data/PNat/Defs.lean

Modified Mathlib/Init/Data/Int/Order.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

deleted def Nat.iterate

Renamed Mathlib/Init/Algebra/Order.lean to Mathlib/Init/Order/Defs.lean

Renamed Mathlib/Init/Algebra/Functions.lean to Mathlib/Init/Order/LinearOrder.lean

Modified Mathlib/Logic/Function/Basic.lean

deleted theorem Function.involutive_iff_iter_2_eq_id

Modified Mathlib/Logic/Function/Iterate.lean

added theorem Function.involutive_iff_iter_2_eq_id

added def Nat.iterate

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Lattice.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Tactic/Basic.lean

Modified Mathlib/Tactic/GCongr/Core.lean

Modified Mathlib/Tactic/PushNeg.lean

Modified test/Tauto.lean

Modified test/push_neg.lean