natCast_mul_right

Mathlib.Data.Nat.Cast.Commute

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

English

If h is a Commute a b, then for any n, Commute a (n*b).

Русский

Если h является перестановкой a и b, то для любого n выполняется Commute a (n*b).

LaTeX

$$$$ \text{Commute } a (n\cdot b) $$$$

Lean4

@[simp]
theorem natCast_mul_right (h : Commute a b) (n : ℕ) : Commute a (n * b) :=
  SemiconjBy.natCast_mul_right h n

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

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

Разделы

Аффилиация

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