Mathlib v3 is deprecated. Go to Mathlib v4

Theorem and_and_and_comm

Modification history

2021-10-01 13:24
src/logic/basic.lean
feat(order/locally_finite): introduce locally finite orders (#9464) …
Added and_and_and_commView on Github →