mathlib
d8b0d1a9 - chore(algebra/big_operators): avoid 'abel' tactic (#9833)

Commit
4 years ago
chore(algebra/big_operators): avoid 'abel' tactic (#9833) I'd like to add an import ` algebra.euclidean_domain` → `algebra.associated` in #9606, so this removes the dependency in the other direction (`algebra.associated` → `algebra.big_operators.basic` → `tactic.abel` → `tactic.norm_num` → `data.rat.cast` → `data.rat.order` → `data.rat.basic` → ` algebra.euclidean_domain`). Fortunately, the dependency on `abel` was quite shallow here.
Parents
Loading