eq_top_of_pow

Mathlib.Algebra.Order.Ring.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.eq_top_of_pow

English

If x^n = ⊤, then x = ⊤; i.e., top is detected by any positive power.

Русский

Если x^n = ⊤, то x = ⊤; то есть ⊤ определяется положительной степенью.

LaTeX

$$$ x^n = \\top \\Rightarrow x = \\top $$$

Lean4

theorem eq_top_of_pow (n : ℕ) (hx : x ^ n = ⊤) : x = ⊤ :=
  (pow_eq_top_iff.1 hx).1

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

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

Разделы

Аффилиация

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