Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.nontrivial_at

Modification history

2020-10-30 14:20
src/logic/nontrivial.lean
feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)
Added pi.nontrivial_atView on Github →