Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-25 14:10 a239cd3e

View on Github →

feat(algebra/order/kleene) : Kleene algebras (#17965) Define idempotent semirings and Kleene algebras, which are used extensively in the theory of computation.

Estimated changes

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_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 pi.kstar_apply
added theorem pi.kstar_def
added theorem pow_le_kstar
added theorem prod.fst_kstar
added theorem prod.kstar_def
added theorem prod.snd_kstar
deleted theorem language.join_mem_star
added theorem language.kstar_def
added theorem language.map_kstar
deleted theorem language.map_star
modified theorem language.mem_add
added theorem language.mem_kstar
deleted theorem language.mem_star
added theorem language.nil_mem_kstar
deleted theorem language.nil_mem_star
deleted def language.star
deleted theorem language.star_def
deleted theorem language.star_eq_supr_pow