mathlib
46ae64dc - chore(group_theory/group_action/prod): Fix typo in `to_additive` attribute. (#17930)

Commit
3 years ago
chore(group_theory/group_action/prod): Fix typo in `to_additive` attribute. (#17930)
Author
Parents
Loading