mk_zero

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.mk_zero

English

In DivisibleHull, mk 0 s equals the zero element for any s in ℕ+.

Русский

В DivisibleHull элемент mk 0 s равен нулю независимо от s ∈ ℕ+.

LaTeX

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

Lean4

@[simp]
theorem mk_zero (s : ℕ+) : mk (0 : M) s = 0 := by simp [mk]

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

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

Разделы

Аффилиация

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