ofNat_left

Mathlib.Data.Nat.Cast.Commute

URI: https://scilib.ai/kg/mathlib#Commute.ofNat_left

English

If n ≥ 2, then OfNat.ofNat n commutes with any x in α.

Русский

Если n ≥ 2, то OfNat.ofNat n коммутирует с любым x в α.

LaTeX

$$$$ \operatorname{OfNat}(n) \cdot x = x \cdot \operatorname{OfNat}(n) $$$$

Lean4

theorem _root_.Commute.ofNat_left (n : ℕ) [n.AtLeastTwo] (x : α) : Commute (OfNat.ofNat n) x :=
  n.cast_commute x

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

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

Разделы

Аффилиация

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