toContinuousLinearEquivOfDetNeZero_apply

English

For a linear map f ∈ E →L[𝕜] E with det ≠ 0, the underlying linear map of the associated continuous linear equivalence f.toContinuousLinearEquivOfDetNeZero hf is f itself.

Русский

Для отображения f ∈ E →L[𝕜] E с det ≠ 0, связное линейное эквивалентное отображение f.toContinuousLinearEquivOfDetNeZero hf имеет ту же линейную часть, что и f.

LaTeX

$$$(f.toContinuousLinearEquivOfDetNeZero \\!\\; hf).toLinearMap = f$$$

Lean4

@[simp]
theorem toContinuousLinearEquivOfDetNeZero_apply (f : E →L[𝕜] E) (hf : f.det ≠ 0) (x : E) :
    f.toContinuousLinearEquivOfDetNeZero hf x = f x :=
  rfl

Похожие утверждения