Theorem: Algebra.TensorProduct.coe_map_id₂ (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
S' : Type u_3
inst✝⁵ : Semiring S
inst✝⁴ : Semiring S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
φ : S →ₐ[R] S'
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ⇑(map φ (AlgHom.id R A)) = ⇑(LinearMap.rTensor A φ.toLinearMap)
Tactic:
rfl
State after:
no goals