toAddMonoidHom_injective — Mathlib

English

The map sending a σ-linear map to its additive monoid hom is injective.

Русский

Отображение, отправляющее σ-линейное отображение в аддитивную однородную гомоморфную структуру, инъективно.

LaTeX

$$$ \text{Injective } (\text{toAddMonoidHom} : (M \to_σ M_3) \to M \to_+ M_3) $$$

Lean4

theorem toAddMonoidHom_injective : Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃) := fun fₗ gₗ h ↦
  ext <| (DFunLike.congr_fun h : ∀ x, fₗ.toAddMonoidHom x = gₗ.toAddMonoidHom x)

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