Structures · Algebra

KleeneAlgebra

A Kleene algebra is an idempotent semiring with an additional unary operator kstar (for Kleene star) that satisfies the following properties: * 1 ≤ a∗ * a * a∗ ≤ a∗ * a∗ * a ≤ a∗ * If b * a ≤ b, then b * a∗ ≤ b * If a * b ≤ b, then a∗ * b ≤ b

Defined in

Mathlib.Algebra.Order.Kleene

Shape

One type argument · adds one_le_kstar, mul_kstar_le_kstar, kstar_mul_le_kstar, mul_kstar_le_self, kstar_mul_le_self