Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-02 15:06 4bcba0da

View on Github →

chore(algebra/order/group/defs): split file (#17787) Splits:

  • algebra/order/group/defs.lean
  • algebra/group/with_one.lean
  • algebra/order/monoid/with_zero.lean This will get us unstuck on the mathlib4 port, moving some of the files (about algebraic morphisms and equivalences) that are currently waiting for fixes in Lean 4 off the critical path.

Estimated changes

added def with_one.lift
added theorem with_one.lift_coe
added theorem with_one.lift_one
added theorem with_one.lift_unique
added def with_one.map
added theorem with_one.map_coe
added theorem with_one.map_comp
added theorem with_one.map_id
added theorem with_one.map_map
deleted def with_one.lift
deleted theorem with_one.lift_coe
deleted theorem with_one.lift_one
deleted theorem with_one.lift_unique
deleted def with_one.map
deleted theorem with_one.map_coe
deleted theorem with_one.map_comp
deleted theorem with_one.map_id
deleted theorem with_one.map_map
deleted theorem inv_le'
deleted theorem le_inv'
deleted def order_iso.inv
deleted def order_iso.mul_left
deleted theorem order_iso.mul_left_symm
deleted def order_iso.mul_right
deleted theorem order_iso.mul_right_symm
added theorem inv_le'
added theorem le_inv'
added def order_iso.inv