natCast_mul_self

Mathlib.Data.Nat.Cast.Commute

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

English

Self natCast mul: Commute (m*a) (n*a) for Nat cast values m, n.

Русский

Самая natCast умножение: Commute (m*a) (n*a) для чисел m, n.

LaTeX

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

Lean4

theorem natCast_mul_self : Commute (n * a) a :=
  (Commute.refl a).natCast_mul_left n

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

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

Разделы

Аффилиация

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