natCast_mul_left

Mathlib.Data.Nat.Cast.Commute

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

English

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

Русский

Если h является Commute a b, тогда Commute (n*a) b.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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