mathlib
a5f4cf53 - fix(algebra/ring_quot): fix a diamond in the int-smul action (#14226)

Commit

3 years ago

fix(algebra/ring_quot): fix a diamond in the int-smul action (#14226) We already handle the `nsmul` diamond correctly in the lines above

Author

eric-wieser

Parents