mathlib3

4b676457 - chore(algebra/ring_quot): provide an explicit npow field (#14349)

chore(algebra/ring_quot): provide an explicit npow field (#14349) While this probably shouldn't matter since `ring_quot` is irreducible, this matches what we do for `nsmul` and `zsmul`.