pow_two

Mathlib.Algebra.Group.Defs

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

← MathLib Explorer

English

For any a ∈ M, a^{2} = a · a.

Русский

Для любого a ∈ M верно a^{2} = a · a.

LaTeX

$$$a^{2} = a \\cdot a$$$

Lean4

/-- Note that most of the lemmas about powers of two refer to it as `sq`. -/
@[to_additive two_nsmul]
theorem pow_two (a : M) : a ^ 2 = a * a := by
  rw [pow_succ, pow_one]
    -- TODO: Should `alias` automatically transfer `to_additive` statements?

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

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

Разделы

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

Аффилиация

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