feat(ring_theory/valuation/valuation_subring): pointwise left actions via `map` (#16080)
feat(ring_theory/valuation/valuation_subring): pointwise left actions via `map` (#16080)

This copies over the API from the pointwise actions on subrings, with the action on a valuation subring just acting on the underlying subring.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Working.20on.20Frobenius.20elements/near/293810759)





leanprover-community/mathlib,leanprover-community/mathlib