R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x - ↑(toCotangent I) y = 0 ↔ ↑x - ↑y ∈ I ^ 2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x = ↑(toCotangent I) y ↔ ↑x - ↑y ∈ I ^ 2
rw [← sub_eq_zero]
no goals
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x - ↑(toCotangent I) y = 0 ↔ ↑x - ↑y ∈ I ^ 2
exact I.mem_toCotangent_ker