dpow_smul_right

Mathlib.RingTheory.DividedPowers.Basic

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

English

The right-smul version: hI.dpow n (a • b) = a·? (convention) but equals hI.dpow n a • b^n.

Русский

Правая формула умножения: hI.dpow n (a • b) = hI.dpow n a • b^n.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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