self_natCast_mul

Mathlib.Data.Nat.Cast.Commute

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

English

Commute a with n*a for any a and n.

Русский

Коммутативность a и n*a для любых a и n.

LaTeX

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

Lean4

theorem self_natCast_mul : Commute a (n * a) :=
  (Commute.refl a).natCast_mul_right n

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

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

Разделы

Аффилиация

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