mathlib3
b6fa37ed - chore(ring_theory/adjoin_root): remove duplicate namespace (#15775)

Commit

3 years ago

chore(ring_theory/adjoin_root): remove duplicate namespace (#15775)

Author

ericrbg

ericrbg

Parents

Loading