Commit 2023-02-13 09:59 0efa8483

View on Github →

feat: port Algebra.Order.Kleene (#2164)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Kleene.lean

added def IdemSemiring.ofSemiring

added theorem Pi.kstar_apply

added theorem Pi.kstar_def

added theorem Prod.fst_kstar

added theorem Prod.kstar_def

added theorem Prod.snd_kstar

added theorem add_eq_left_iff_le

added theorem add_eq_right_iff_le

added theorem add_eq_sup

added theorem add_idem

added theorem add_le

added theorem add_le_iff

added theorem kstar_eq_one

added theorem kstar_eq_self

added theorem kstar_idem

added theorem kstar_le_of_mul_le_left

added theorem kstar_le_of_mul_le_right

added theorem kstar_mono

added theorem kstar_mul_kstar

added theorem kstar_mul_le

added theorem kstar_mul_le_kstar

added theorem kstar_mul_le_self

added theorem kstar_one

added theorem kstar_zero

added theorem le_kstar

added theorem mul_kstar_le

added theorem mul_kstar_le_kstar

added theorem mul_kstar_le_self

added theorem nsmul_eq_self

added theorem one_le_kstar

added theorem pow_le_kstar