zero_smul

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.Sheafify.zero_smul

← MathLib Explorer

English

The action of 1 on any m is m.

Русский

Действие единицы на элементе m даёт сам m.

LaTeX

$$$ one\_smul: smul α φ 1 m = m $$$

Lean4

protected theorem zero_smul : smul α φ 0 m = 0 :=
  by
  apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)
  rintro Y f ⟨m₀, hm₀⟩
  rw [map_smul_eq α φ 0 m f.op 0 (by simp) m₀ hm₀, zero_smul, map_zero, (A.val.map f.op).hom.map_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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