English
The structure on PerfectClosure(K,p) makes it a division ring (hence contains multiplicative inverses).
Русский
Строение PerfectClosure(K,p) образует делитель-кольцо (существуют обратные элементы по умножению).
LaTeX
$$$\mathrm{DivisionRing}(\mathrm{PerfectClosure}(K,p)).$$$
Lean4
instance instDivisionRing : DivisionRing (PerfectClosure K p)
where
mul_inv_cancel
e :=
induction_on e fun ⟨m, x⟩ H ↦ by
have := mt (eq_iff _ _ _ _).2 H
rw [mk_inv, mk_mul_mk]
refine (eq_iff K p _ _).2 ?_
simp only [iterate_map_one, iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at this ⊢
rw [mul_inv_cancel₀ this, iterate_map_one]
inv_zero := congr_arg (Quot.mk (R K p)) (by rw [inv_zero])
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
