zpow_natCast_sub_natCast

Mathlib.Algebra.Group.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive natCast_sub_natCast_zsmul]
theorem zpow_natCast_sub_natCast (a : G) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n := by
  simpa [div_eq_mul_inv] using zpow_sub a m n

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

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

Разделы

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

Аффилиация

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