toLinearMap_ofBijective — Mathlib

English

The linear map underlying the promoted equivalence equals the original algebra hom's linear map.

Русский

Линейное отображение, лежащее в основе продвинутой эквивалентности, равно линейному отображению исходного алгебраического гомоморфизма.

LaTeX

$$$ (\\mathrm{ofBijective}(f, hf)).toLinearMap = f $$$

Lean4

@[simp]
theorem toLinearMap_ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : (ofBijective f hf).toLinearMap = f :=
  rfl

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