map_zero

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.map_zero

← MathLib Explorer

English

The map f sends zero to zero in LocalizationMap; i.e., f(0) = 0.

Русский

Отображение f обрамляет ноль нулю: f(0) = 0.

LaTeX

$$$f(0) = 0$$$

Lean4

protected theorem map_zero (f : LocalizationMap S N) : f 0 = 0 :=
  by
  have ⟨ms, eq⟩ := f.surj 0
  rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]

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

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

Разделы

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

Аффилиация

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