dpow_smul

Mathlib.RingTheory.DividedPowers.Basic

URI: https://scilib.ai/kg/mathlib#DividedPowers.dpow_smul

English

Scaling rule: dpow n (b • a) equals b^n • dpow n a under ha: a ∈ I.

Русский

Правило масштабирования: dpow n (b • a) = b^n • dpow n a при ha: a ∈ I.

LaTeX

$$$$ hI.dpow n (b \\cdot a) = b^n \\cdot hI.dpow n a $$$$

Lean4

theorem dpow_smul {n : ℕ} (ha : a ∈ I) : hI.dpow n (b • a) = b ^ n • hI.dpow n a := by
  simp only [smul_eq_mul, hI.dpow_mul, ha]

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

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

Разделы

Аффилиация

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