one_div_pow

Mathlib.Algebra.Group.Basic

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

English

For any a ∈ α and n ∈ ℕ, (1 / a)^n = 1 / a^n.

Русский

Для любого a ∈ α и n ∈ ℕ, (1 / a)^n = 1 / a^n.

LaTeX

$$$\\left(\\frac{1}{a}\\right)^n = \\frac{1}{a^n}$$$

Lean4

@[to_additive nsmul_zero_sub]
theorem one_div_pow (a : α) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n := by simp only [one_div, inv_pow]

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

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

Разделы

Аффилиация

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