mathlib
50ee3d56 - feat(ring_theory/roots_of_unity): coe_injective (#11793)

Commit

4 years ago

feat(ring_theory/roots_of_unity): coe_injective (#11793) from flt-regular

Author

ericrbg

ericrbg

Parents

Loading