English
In the completion hat K, every nonzero element x has a multiplicative inverse hatInv x, and x * hatInv x = 1.
Русский
В дополнении hat K любое ненулевое x имеет обратное hatInv x, и x · hatInv x = 1.
LaTeX
$$$x \neq 0 \;\Rightarrow\; x \cdot \hatInv x = 1$$$
Lean4
theorem mul_hatInv_cancel {x : hat K} (x_ne : x ≠ 0) : x * hatInv x = 1 :=
by
haveI : T1Space (hat K) := T2Space.t1Space
let f := fun x : hat K => x * hatInv x
let c := (fun (x : K) => (x : hat K))
change f x = 1
have cont : ContinuousAt f x := by fun_prop (disch := assumption)
have clo : x ∈ closure (c '' {0}ᶜ) := by
have := isDenseInducing_coe.dense x
rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm, image_union] at this
apply mem_closure_of_mem_closure_union this
rw [image_singleton]
exact compl_singleton_mem_nhds x_ne
have fxclo : f x ∈ closure (f '' (c '' {0}ᶜ)) := mem_closure_image cont clo
have : f '' (c '' {0}ᶜ) ⊆ { 1 } := by
rw [image_image]
rintro _ ⟨z, z_ne, rfl⟩
rw [mem_singleton_iff]
rw [mem_compl_singleton_iff] at z_ne
dsimp [f]
rw [hatInv_extends z_ne, ← coe_mul]
rw [mul_inv_cancel₀ z_ne, coe_one]
replace fxclo := closure_mono this fxclo
rwa [closure_singleton, mem_singleton_iff] at fxclo
