mathlib
ed833060 - feat(set/prod): decidable mem instance for diagonal (#15846)

Commit

3 years ago

feat(set/prod): decidable mem instance for diagonal (#15846) Membership in `diagonal A` is decidable if we have `decidable_eq A`

Author

dtumad

Parents