Commit 2022-12-01 10:59 fe45d2dc

View on Github →

feat: port Algebra.Order.Monoid.Canonical.Defs (#778) mathlib SHA: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a Porting Notes: 1. Haven't touched protect_proj. If someone knows what to do to fix this, please feel free. 2. LinearOrder.toLattice is found in Order.Lattice which is both not ported yet and not imported.

  1. simp_rw seems to be more aggressive in lean4, so a proof was rewritten to just use rw alone.
  2. simpa seemed to continue to try and solve a goal after it had already been solved.
  3. one_lt_mul_iff needed an additional rfl to solve. This wasn't needed in lean3.
  4. Some simp lemmas are not simp-normal form. I have not debugged any of these yet.
  5. Further documentation is needed. If anyone wants to add them, please feel free.

Estimated changes

added theorem NeZero.of_gt
added theorem NeZero.pos
added theorem bot_eq_one'
added theorem bot_eq_one
added theorem eq_one_or_one_lt
added theorem le_iff_exists_mul'
added theorem le_iff_exists_mul
added theorem le_mul_left
added theorem le_mul_right
added theorem le_mul_self
added theorem le_of_mul_le_left
added theorem le_of_mul_le_right
added theorem le_one_iff_eq_one
added theorem le_self_mul
added theorem lt_iff_exists_mul
added theorem min_mul_distrib'
added theorem min_mul_distrib
added theorem min_one
added theorem mul_eq_one_iff
added theorem one_le
added theorem one_lt_iff_ne_one
added theorem one_lt_mul_iff
added theorem one_min
added theorem pos_of_gt
added theorem self_le_mul_left
added theorem self_le_mul_right
deleted theorem zero_le