mathlib3
0a78dc41 - chore(algebra/*): add missing ancestor attributes (#17509)

Commit

3 years ago

chore(algebra/*): add missing ancestor attributes (#17509) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents