toContinuousAddMonoidHom_injective

English

Injectivity of the coercion to semilinear maps; same as 196407.

Русский

Инъективность приведения к полусемилинейным отображениям; то же, что и 196407.

LaTeX

$$$(f : M_1 \toSL[\sigma_{12}] M_2) = g \;\Leftrightarrow\; f = g$$$

Lean4

theorem toContinuousAddMonoidHom_injective :
    Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → ContinuousAddMonoidHom M₁ M₂) :=
  (DFunLike.coe_injective.of_comp_iff _).1 DFunLike.coe_injective

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