op_intCast

Mathlib.Algebra.Ring.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.op_intCast

English

For any integer n, op(n in R) equals n in the opposite sense.

Русский

Для любого целого числа n операция op(n) равна n в противоположном кольце.

LaTeX

$$$\operatorname{op}(n : R) = n$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem op_intCast [IntCast R] (n : ℤ) : op (n : R) = n :=
  rfl

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

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

Разделы

Аффилиация

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