F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x * y⁻¹ ∈ S
F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x / y ∈ S
rw [div_eq_mul_inv]
no goals
F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x * y⁻¹ ∈ S
exact hS.toIsSubring.toIsSubmonoid.mul_mem hx (hS.inv_mem hy)