div_pow

Mathlib.Algebra.Group.Basic

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

English

In a DivisionMonoid, (a/b)^n = a^n / b^n for all a,b and n ∈ ℕ.

Русский

В делимом полугруппе для любых a,b и n ∈ ℕ выполняется (a/b)^n = a^n / b^n.

LaTeX

$$$(\tfrac{a}{b})^{n} = \tfrac{a^{n}}{b^{n}}$$$

Lean4

@[to_additive nsmul_sub]
theorem div_pow (a b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n := by simp only [div_eq_mul_inv, mul_pow, inv_pow]

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

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

Разделы

Аффилиация

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