natCast_mul_natCast_mul

Mathlib.Data.Nat.Cast.Commute

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

English

Given h, m, n, SemiconjBy a x y respects both left and right natCast operations: SemiconjBy a (m.cast x) (n.cast y).

Русский

Дано h; SemiconjBy сохраняет natCast слева и справа: SemiconjBy a (m.cast x) (n.cast y).

LaTeX

$$$$ \text{SemiconjBy } a (m.cast \; x) (n.cast \; y) $$$$

Lean4

theorem natCast_mul_natCast_mul (h : SemiconjBy a x y) (m n : ℕ) : SemiconjBy (m * a) (n * x) (n * y) := by simp [h]

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

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

Разделы

Аффилиация

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