English
A continuous linear equivalence f: M ≃L[R] M determines a unit in the algebra of endomorphisms (M →L[R] M).
Русский
Непрерывное линейное эквивалентное отображение f: M ≃L[R] M определяет единичный элемент в алгебре концевых отображений (M →L[R] M).
LaTeX
$$$\\text{toUnit}(f) : (M \\toL[R] M)^{\\times}$$$
Lean4
/-- An invertible continuous linear map `f` determines a continuous equivalence from `M` to itself.
-/
def ofUnit (f : (M →L[R] M)ˣ) : M ≃L[R] M
where
toLinearEquiv :=
{ toFun := f.val
map_add' := by simp
map_smul' := by simp
invFun := f.inv
left_inv := fun x =>
show (f.inv * f.val) x = x by
rw [f.inv_val]
simp
right_inv := fun x =>
show (f.val * f.inv) x = x by
rw [f.val_inv]
simp }
continuous_toFun := f.val.continuous
continuous_invFun := f.inv.continuous
