Commit 2022-12-18 21:17 a9a1f7d7

View on Github →

chore: update lean4/std4 (#1096)

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Opposite.lean

Modified Mathlib/Algebra/GroupPower/Order.lean

Modified Mathlib/Algebra/GroupPower/Ring.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/Algebra/Order/Invertible.lean

modified theorem invOf_lt_zero

modified theorem invOf_nonpos

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

Modified Mathlib/Algebra/Order/Sub/Canonical.lean

Modified Mathlib/CategoryTheory/Iso.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/Nat/Basic.lean

modified theorem Nat.lt_one_add_iff

modified theorem Nat.one_add_le_iff

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

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Data/Set/Sigma.lean

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

deleted theorem Int.neg_negSucc

Modified Mathlib/Init/Set.lean

Modified Mathlib/Logic/Basic.lean

modified theorem xor_iff_iff_not

modified theorem xor_iff_not_iff'

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Mathport/Notation.lean

Modified Mathlib/Order/Bounded.lean

Modified Mathlib/Order/BoundedOrder.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/CompleteLattice.lean

Modified Mathlib/Order/Disjoint.lean

Modified Mathlib/Order/Heyting/Basic.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/Iterate.lean

Modified Mathlib/Order/MinMax.lean

Modified Mathlib/Order/PropInstances.lean

Modified Mathlib/Order/SymmDiff.lean

Modified Mathlib/Order/WithBot.lean

Modified lake-manifest.json

Modified lean-toolchain