R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
skip
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
this : Field (R ⧸ I) := Quotient.field I
⊢ IsMaximal ⊥
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
letI := Quotient.field I
no goals
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
this : Field (R ⧸ I) := Quotient.field I
⊢ IsMaximal ⊥
exact bot_isMaximal