Mathlib v3 is deprecated. Go to Mathlib v4

Theorem decidable.and_or_imp

Modification history

2021-12-06 22:38
src/logic/basic.lean
feat(algebra/geom_sum): criteria for 0 < geom_sum (#10567)
Added decidable.and_or_impView on Github →