Commit 2023-08-08 05:54 1d493fee

View on Github →

feat(Algebra/GroupPower): weaken TC assumptions (#6389)

  • Assume OrderedSemiring instead of StrictOrderedSemiring here and there.
  • Add @[simp] to zsmul_one.
  • Add exists_lt_nsmul.

Estimated changes

added theorem exists_lt_nsmul
modified theorem exists_nat_ge