div_zpow — Mathlib

English

Let α be a commutative division monoid. For any elements a, b ∈ α and any integer n ∈ ℤ, (a / b)^n = a^n / b^n.

Русский

Пусть α — коммутативный моноид с операцией деления. Для любых a, b ∈ α и любого целого n ∈ ℤ выполняется (a / b)^n = a^n / b^n.

LaTeX

$$$ (a / b)^n = a^n / b^n $$$

Lean4

@[to_additive zsmul_sub]
theorem div_zpow (a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n := by simp only [div_eq_mul_inv, mul_zpow, inv_zpow]

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