natCast_mul_natCast_mul

Mathlib.Data.Nat.Cast.Commute

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

English

For h, and m, n, Commute a b implies Commute (cast m a) (cast n b).

Русский

Для h и чисел m, n, перестановность сохраняется между наслоениями приведения.

LaTeX

$$$$ \text{Commute } a b \rightarrow \text{Commute } (m.cast \; a) (n.cast \; b) $$$$

Lean4

theorem natCast_mul_natCast_mul (h : Commute a b) (m n : ℕ) : Commute (m * a) (n * b) := by simp [h]

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

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

Разделы

Аффилиация

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