zpow_one_sub_natCast

Mathlib.Algebra.Group.Basic

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

← MathLib Explorer

English

Let a ∈ G and n ∈ ℕ. Then a^{1-n} = a / a^n.

Русский

Пусть a ∈ G и n ∈ ℕ. Тогда a^{1-n} = a / a^n.

LaTeX

$$$\forall a \in G,\ \forall n \in \mathbb{N},\ a^{1-n} = a / a^{n}$$$

Lean4

@[to_additive one_sub_natCast_zsmul]
theorem zpow_one_sub_natCast (a : G) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n := by
  simpa [div_eq_mul_inv] using zpow_sub a 1 n

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

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

Разделы

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

Аффилиация

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