algebraMap_toAlgebra — Mathlib

English

In the same setting, the equality of the scalar action with multiplication is formalized by a proof of equality.

Русский

В той же настройке равенство действия скаляра и умножения фиксируется доказательством равенства.

LaTeX

$$$r \cdot s = i(r) \cdot s$ (by construction).$$

Lean4

theorem algebraMap_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
    @algebraMap R S _ _ i.toAlgebra = i :=
  rfl

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