mathlib3
7188d806 - chore(algebra/pi_tensor_product): Replace use of classical with decidable_eq (#5880)

Commit

5 years ago

chore(algebra/pi_tensor_product): Replace use of classical with decidable_eq (#5880) This makes it consistent with `multilinear_map`, which also uses explicit decidability assumptions

Author

eric-wieser

Parents

1dfa81a1

mathlib3 7188d806 - chore(algebra/pi_tensor_product): Replace use of classical with decidable_eq (#5880)

mathlib3
7188d806 - chore(algebra/pi_tensor_product): Replace use of classical with decidable_eq (#5880)