zero_mk

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#LocalizedModule.zero_mk

English

The map mk sends zero to zero in the localized module.

Русский

Отображение mk отправляет ноль в ноль локализованного модуля.

LaTeX

$$$\\text{zero\_mk}(s) : mk(0:M,s) = 0$.$$

Lean4

@[simp]
theorem zero_mk (s : S) : mk (0 : M) s = 0 :=
  mk_eq.mpr ⟨1, by rw [one_smul, smul_zero, smul_zero, one_smul]⟩

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

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

Разделы

Аффилиация

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