mathlib3
45e412da - chore(number_theory/number_field): remove duplicate name (#15400)

Commit

3 years ago

chore(number_theory/number_field): remove duplicate name (#15400)

Author

ericrbg

ericrbg

Parents

Loading