Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 01:25 b8b18fa5

View on Github →

feat(order/complete_boolean_algebra): A frame is distributive (#15340) frame α/coframe α imply distrib_lattice α.

Estimated changes