Theorems · Definition · ring theory
KStar.kstar
{α : Type u_5} → [self : KStar α] → α → αThe Kleene star operator on a Kleene algebra
- Defined in
- Mathlib.Algebra.Order.Kleene
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- KStar
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- KStarstatement and proof · cited by 0
Cited by55
Results whose statement or proof uses this declaration.
- one_le_kstarstatement · cited by 8
- Language.kstar_eq_iSup_powstatement · cited by 5
- le_kstarstatement · cited by 3
- kstar_le_of_mul_le_leftstatement and proof · cited by 3
- kstar_mul_le_kstarstatement · cited by 3
- mul_kstar_lestatement and proof · cited by 2
- mul_kstar_le_kstarstatement · cited by 2
- mul_kstar_le_selfstatement · cited by 2
- Language.one_add_self_mul_kstar_eq_kstarstatement · cited by 2
- kstar_eq_onestatement · cited by 2
- kstar_mul_kstarstatement · cited by 2
- kstar_mul_lestatement and proof · cited by 2