case ofNat
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s t : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.ofNat a✝ ∈ s

case negSucc
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s t : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.negSucc a✝ ∈ s
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s t : Subfield K
x : K
hx : x ∈ s
n : ℤ
⊢ x ^ n ∈ s
cases n
no goals
case ofNat
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s t : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.ofNat a✝ ∈ s
simpa using s.pow_mem hx _
no goals
case negSucc
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s t : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.negSucc a✝ ∈ s
simpa [pow_succ] using s.inv_mem (s.mul_mem hx (s.pow_mem hx _))