cast_sub

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#ZNum.cast_sub

English

Embedding preserves subtraction: ((m - n) : α) = m - n.

Русский

Встраивание сохраняет вычитание: ((m - n) : α) = m - n.

LaTeX

$$$$\forall m,n \in ZNum,\ ((m - n : ZNum) : α) = (m : α) - (n : α).$$$$

Lean4

@[simp, norm_cast]
theorem cast_sub [AddCommGroupWithOne α] (m n) : ((m - n : ZNum) : α) = m - n := by simp [sub_eq_neg_add]

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

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

Разделы

Аффилиация

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