mathlib
ad6d4764 - refactor(ring_theory/derivation): remove old_structure_cmd (#9724)

Commit

4 years ago

refactor(ring_theory/derivation): remove old_structure_cmd (#9724) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents