primitive_roots): generalisation linter (#16013)

Commit

3 years ago

chore(number_theory/cyclotomic/primitive_roots): generalisation linter (#16013) Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author

ericrbg

Parents

26c2c38d

mathlib 32258e92 - chore(number_theory/cyclotomic/primitive_roots): generalisation linter (#16013)

mathlib
32258e92 - chore(number_theory/cyclotomic/primitive_roots): generalisation linter (#16013)