pow

Mathlib.Algebra.Regular.Basic

URI: https://scilib.ai/kg/mathlib#IsRegular.pow

← MathLib Explorer

English

If ra is regular, then a^n is regular for any n.

Русский

Если a регулярен, то a^n регулярна для любого n.

LaTeX

$$$ IsRegular a \rightarrow IsRegular (a^n) $$$

Lean4

/-- Any power of a regular element is regular. -/
@[to_additive]
theorem pow (n : ℕ) (ra : IsRegular a) : IsRegular (a ^ n) :=
  ⟨IsLeftRegular.pow n ra.left, IsRightRegular.pow n ra.right⟩

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

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

Разделы

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

Аффилиация

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