𝕜 : Type u_1
𝕝 : Type ?u.39565
E : Type u_2
ι : Sort ?u.39571
κ : ι → Sort ?u.39576
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ + -s₂) (t₁ + -t₂)
𝕜 : Type u_1
𝕝 : Type ?u.39565
E : Type u_2
ι : Sort ?u.39571
κ : ι → Sort ?u.39576
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ - s₂) (t₁ - t₂)
simp_rw [sub_eq_add_neg]
no goals
𝕜 : Type u_1
𝕝 : Type ?u.39565
E : Type u_2
ι : Sort ?u.39571
κ : ι → Sort ?u.39576
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ + -s₂) (t₁ + -t₂)
exact h₁.add h₂.neg