ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ val y1 + -val y2 = val y1 - val y2
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ val (y1 - y2) = val y1 - val y2
rw [show y1 - y2 = y1 + -y2 from rfl, add_val, neg_val]
no goals
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ val y1 + -val y2 = val y1 - val y2
rfl