R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ LocalRing R
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
⊢ LocalRing R
haveI : Nontrivial R := pullback_nonzero f f.map_zero f.map_one
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ LocalRing R
apply LocalRing.of_nonunits_add
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
intro a b
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ ↑f a ∈ nonunits S → ↑f b ∈ nonunits S → ↑f a + ↑f b ∈ nonunits S
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
simp_rw [← map_mem_nonunits_iff f, f.map_add]
no goals
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ ↑f a ∈ nonunits S → ↑f b ∈ nonunits S → ↑f a + ↑f b ∈ nonunits S
exact LocalRing.nonunits_add