Theorem kstar_zero

Modification history

2026-04-29 14:11

Mathlib/Algebra/Order/Kleene.lean

chore: make argument in `zero_le`/`one_le` implicit (#38148) …

Modified kstar_zero View on Github →

2024-03-28 11:53

Mathlib/Algebra/Order/Kleene.lean

chore: Reduce scope of `LinearOrderedCommGroupWithZero` (#11716) …

Modified kstar_zero View on Github →

2023-02-13 09:59

Mathlib/Algebra/Order/Kleene.lean

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

Added kstar_zero View on Github →