mk_mul

Mathlib.Algebra.Order.Ring.Archimedean

URI: https://scilib.ai/kg/mathlib#ArchimedeanClass.mk_mul

English

mk(x^n) equals n times mk x, i.e., the class element for x^n is the n-fold sum of mk x.

Русский

mk(х^n) равно n раз mk x, то есть элемент ArchimedeanClass, соответствующий x^n, равен сумме из n слагаемых mk x.

LaTeX

$$$$ \operatorname{mk}(x^n) = n \cdot \operatorname{mk}(x). $$$$

Lean4

@[simp]
theorem mk_mul (x y : R) : mk (x * y) = mk x + mk y :=
  rfl

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

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

Разделы

Аффилиация

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