instZero

Mathlib.GroupTheory.GroupAction.Hom

URI: https://scilib.ai/kg/mathlib#DistribMulActionHom.instZero

English

If ring-homomorphisms f,g are compatible with a σ-action, and f(1) = g(1), then f = g.

Русский

Если кольцевые гомоморфизмы f,g совместимы с действием σ и f(1) = g(1), то f = g.

LaTeX

$$$ f(1) = g(1) \\Rightarrow f = g $$$

Lean4

instance : Zero (A →ₑ+[φ] B) :=
  ⟨{ (0 : A →+ B) with map_smul' := fun m _ => by simp }⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru