mathlib

e7d40ef3 - refactor(*): Move an instance to a more appropriate file (#4939)

refactor(*): Move an instance to a more appropriate file (#4939) In its former location, this instance related neither to the section it was the sole resident of, nor even to the file.