mathlib3
5397ac0e - chore(ring_theory/hahn_series): remove redundant instances (#14045)

Commit

3 years ago

chore(ring_theory/hahn_series): remove redundant instances (#14045) Both of these instances can be proved `by apply_instance`

Author

ocfnash

Parents