ofLinearMap_toLinearMap — Mathlib

English

The underlying linear map of the AlgHom built from a linear map f coincides with f: toLinearMap (ofLinearMap f map_one map_mul) = f.

Русский

Линейное отображение, связанное с AlgHom, построенным из линейного отображения f, равно f: toLinearMap (ofLinearMap f map_one map_mul) = f.

LaTeX

$$$$\mathrm{toLinearMap}(\mathrm{ofLinearMap}\ f\ map\_one\ map\_mul) = f.$$$$

Lean4

@[simp]
theorem ofLinearMap_toLinearMap (map_one) (map_mul) : ofLinearMap φ.toLinearMap map_one map_mul = φ :=
  rfl

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