toLinearMap_id — Mathlib

English

The underlying linear map of the identity algebra homomorphism is the identity linear map.

Русский

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

LaTeX

$$$$\text{toLinearMap}(\mathrm{AlgHom.id}\,R\,A) = \text{LinearMap.id}.$$$$

Lean4

@[simp]
theorem toLinearMap_id : toLinearMap (AlgHom.id R A) = LinearMap.id :=
  rfl

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