cast_mul

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#PosNum.cast_mul

← MathLib Explorer

English

For any Num n, the cast of pred n to ℕ equals Nat.pred n.

Русский

Для любого Num n, привод предшественника к ℕ равен Nat.pred n.

LaTeX

$$$\\forall n : \\text{Num}, (\\operatorname{pred} n : \\mathbb{N}) = \\operatorname{Nat.pred} n$$$

Lean4

@[simp, norm_cast]
theorem cast_mul [NonAssocSemiring α] (m n) : ((m * n : PosNum) : α) = m * n := by
  rw [← cast_to_nat, mul_to_nat, Nat.cast_mul, cast_to_nat, cast_to_nat]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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