dpow_eq_of_mem

Mathlib.RingTheory.DividedPowers.RatAlgebra

URI: https://scilib.ai/kg/mathlib#DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem

English

If x ∈ I, then dpow I m x equals inverse(m!) times x^m.

Русский

Если x ∈ I, то dpow_I(m, x) = inverse(m!) · x^m.

LaTeX

$$theorem dpow_eq_of_mem {m : ℕ} {x : A} (hx : x ∈ I) : dpow I m x = inverse (m ! : A) * x ^ m$$

Lean4

theorem dpow_eq_of_mem {m : ℕ} {x : A} (hx : x ∈ I) : dpow I m x = inverse (m ! : A) * x ^ m := by simp [dpow, hx]

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

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

Разделы

Аффилиация

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