mk'_zero

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.mk'_zero

English

For any s ∈ S, f.mk' 0 s = 0; i.e., the representation of zero remains zero under mk'.

Русский

Для любого s ∈ S, f.mk' 0 s = 0; то есть представление нуля через mk' остаётся нулём.

LaTeX

$$$f.mk' 0 s = 0$$$

Lean4

@[simp]
theorem mk'_zero (f : LocalizationMap S N) (s : S) : f.mk' 0 s = 0 := by
  rw [eq_comm, eq_mk'_iff_mul_eq, zero_mul, f.map_zero]

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

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

Разделы

Аффилиация

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