no goals
S : Type ?u.861406
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
m : M
⊢ ↑(algebraMap R' A) 0 + ↑f m = ↑f m
rw [RingHom.map_zero, zero_add]