addVal_mul

Mathlib.RingTheory.DiscreteValuationRing.Basic

URI: https://scilib.ai/kg/mathlib#IsDiscreteValuationRing.addVal_mul

English

Repetition of the exponent equality under unit-corrected power relations for irreducibles.

Русский

Повторение равенства степеней под единичными соответствиями степеней ирредуцируемых.

LaTeX

$$$m = n$$$

Lean4

theorem addVal_mul {a b : R} : addVal R (a * b) = addVal R a + addVal R b :=
  (addVal R).map_mul _ _

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

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

Разделы

Аффилиация

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