no goals
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_1
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
s : Set A
h : Set.EqOn (↑D1) (↑D2) s
x✝ : A
hx✝ : x✝ ∈ ↑(adjoin R s)
x y : A
hx : ↑D1 x = ↑D2 x
hy : ↑D1 y = ↑D2 y
⊢ ↑D1 (x + y) = ↑D2 (x + y)
simp only [map_add, *]
no goals
R : Type u_3
inst✝⁵ : CommSemiring R
A : Type u_1
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
s : Set A
h : Set.EqOn (↑D1) (↑D2) s
x✝ : A
hx✝ : x✝ ∈ ↑(adjoin R s)
x y : A
hx : ↑D1 x = ↑D2 x
hy : ↑D1 y = ↑D2 y
⊢ ↑D1 (x * y) = ↑D2 (x * y)
simp only [leibniz, *]