dpow_mul_right

Mathlib.RingTheory.DividedPowers.Basic

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

English

For ha: a ∈ I, dpow n (a·b) equals dpow n a times b^n, up to commutation.

Русский

Для ha: a ∈ I, dpow n (a·b) = dpow n a · b^n (при условии коммутирования).

LaTeX

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

Lean4

theorem dpow_mul_right {n : ℕ} (ha : a ∈ I) : hI.dpow n (a * b) = hI.dpow n a * b ^ n := by
  rw [mul_comm, hI.dpow_mul ha, mul_comm]

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

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

Разделы

Аффилиация

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