mathlib3
f71e3597 - chore(ring_theory/power_series): avoid id in instances (#3033)

Commit

5 years ago

chore(ring_theory/power_series): avoid id in instances (#3033) The power series instances contain a spurious `id`, that we remove.

Author

sgouezel

Parents