mathlib
70e1ddf2 - introduce old_structure_cmd in group_theory/group_action/defs

Commit

4 years ago

introduce old_structure_cmd in group_theory/group_action/defs

References

adomani_old_has_scalar

Author

adomani

adomani

Parents

Loading