feat(Normed/Ring/WithAbs): apply results relating algebraMaps on WithAbs (#29944)

Author: smmercuri

Mathlib/Analysis/Normed/Ring/WithAbs.lean

@@ -92,9 +92,18 @@ variable {R' : Type*} [CommSemiring R] [Semiring R'] [Algebra R R']
 instance instAlgebra_left (v : AbsoluteValue R S) : Algebra (WithAbs v) R' :=
   inferInstanceAs <| Algebra R R'
 
+theorem algebraMap_left_apply (v : AbsoluteValue R S) (x : WithAbs v) :
+    algebraMap (WithAbs v) R' x = algebraMap R R' (WithAbs.equiv v x) := rfl
+
 instance instAlgebra_right (v : AbsoluteValue R' S) : Algebra R (WithAbs v) :=
   inferInstanceAs <| Algebra R R'
 
+theorem algebraMap_right_apply (v : AbsoluteValue R' S) (x : R) :
+    algebraMap R (WithAbs v) x = WithAbs.equiv v (algebraMap R R' x) := rfl
+
+theorem equiv_algebraMap_apply (v : AbsoluteValue R S) (w : AbsoluteValue R' S) (x : WithAbs v) :
+    equiv w (algebraMap (WithAbs v) (WithAbs w) x) = algebraMap R R' (equiv v x) := rfl
+
 /-- The canonical algebra isomorphism from an `R`-algebra `R'` with an absolute value `v`
 to `R'`. -/
 def algEquiv (v : AbsoluteValue R' S) : (WithAbs v) ≃ₐ[R] R' := AlgEquiv.refl (A₁ := R')