is_localization.mk'_pow

Stream: Is there code for X?

[Nikolas Kuhn]

Do we have something like this for localization of algebras? docs#ring_theory.localization.basic
lemma is_localization.mk'_pow : is_localization.mk' 1 (m^k) = (is_localization.mk' 1 m) ^ k.
Or alternatively, can one get some statement that mk' here is a monoid homomorphism?

I feel like I've seen this before, but couldn't find it anymore...

[Andrew Yang]

docs#is_localization.to_inv_submonoid should be close.