one_div_pow

Mathlib.LinearAlgebra.Matrix.ZPow

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

English

For any A, (1/A)^n = 1/A^n for natural n.

Русский

Для любого A выполняется (1/A)^n = 1/A^n для натурального n.

LaTeX

$$$ (1/A)^n = 1/A^n \quad (n \in \mathbb{N}) $$$

Lean4

theorem one_div_pow {A : M} (n : ℕ) : (1 / A) ^ n = 1 / A ^ n := by simp only [one_div, inv_pow']

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

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

Разделы

Аффилиация

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