one_smul

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

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

← MathLib Explorer

English

The scalar action by zero is zero for any m.

Русский

Действие скаляра нулю на любом элементе равно нулю.

LaTeX

$$$ smul\_zero: smul α φ 0 m = 0 $$$

Lean4

protected theorem one_smul : smul α φ 1 m = m :=
  by
  apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)
  rintro Y f ⟨m₀, hm₀⟩
  rw [← hm₀, map_smul_eq α φ 1 m f.op 1 (by simp) m₀ hm₀, one_smul]

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

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

Разделы

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

Аффилиация

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