pow_zero

Mathlib.Algebra.Group.Defs

URI: https://scilib.ai/kg/mathlib#pow_zero

English

For any Monoid M and any a ∈ M, a^0 = 1.

Русский

Для любого моноида M и любого a ∈ M, a^0 = 1.

LaTeX

$$$\\forall M\\,[Monoid M],\\forall a\\in M:\\ a^{0} = 1$$$

Lean4

@[to_additive (attr := simp high) zero_nsmul]
theorem pow_zero (a : M) : a ^ 0 = 1 :=
  Monoid.npow_zero _

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

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

Разделы

Аффилиация

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