biproducts): Speed up `biprod.column_nonzero_of_iso` (#13383)

Commit

3 years ago

chore(category_theory/preadditive/biproducts): Speed up `biprod.column_nonzero_of_iso` (#13383) From 76s down to 2s. The decidability synthesis in `by_contradiction` is stupidly expensive.

Author

YaelDillies

Parents

4bcc5325

mathlib 5534e246 - chore(category_theory/preadditive/biproducts): Speed up `biprod.column_nonzero_of_iso` (#13383)

mathlib
5534e246 - chore(category_theory/preadditive/biproducts): Speed up `biprod.column_nonzero_of_iso` (#13383)