unit_pow

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#IsUnit.unit_pow

English

The unit corresponding to a raised to the nth power is the nth power of the unit.

Русский

Единица, соответствующая a^n, равна (единица a)^n.

LaTeX

$$$\forall {M} [Monoid M] {a : M} (h : IsUnit a) (n : \mathbb{N}), (h.pow n).unit = h.unit^n$$$

Lean4

@[to_additive]
theorem unit_pow (h : IsUnit a) (n : ℕ) : (h.pow n).unit = h.unit ^ n :=
  Units.ext rfl

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

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

Разделы

Аффилиация

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