Revision #2824 → #3304 · back to history
a67a8d58902d| Field | From #2824 | To #3304 |
|---|---|---|
| note | Mathlib has no `DeMorganAlgebra` or `KleeneAlgebra` (with involution) hierarchy showing `BooleanAlgebra` as a specialization. | Mathlib's `KleeneAlgebra` is the semiring-with-star (regular-expression) notion, not the involutive-lattice Kleene algebra, and there is no `DeMorganAlgebra` hierarchy with `BooleanAlgebra` as a specialization. |
22619010e82d5eb5f091baf2