mathlib
711aa755 - refactor(algebra/gcd_monoid): remove superfluous old_structure_cmd (#9720)

Commit

4 years ago

refactor(algebra/gcd_monoid): remove superfluous old_structure_cmd (#9720) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents