of_zero_ofNat

Mathlib.Algebra.DirectSum.Ring

URI: https://scilib.ai/kg/mathlib#DirectSum.of_zero_ofNat

English

If n is a natural number at least two, then of A 0 ofNat(n) equals ofNat(n).

Русский

Если n является натуральным числом не менее двух, то of A 0 ofNat(n) = ofNat(n).

LaTeX

$$$\text{of}_A(0)\,\text{ofNat}(n) = \text{ofNat}(n)$$$

Lean4

@[simp]
theorem of_zero_ofNat (n : ℕ) [n.AtLeastTwo] : of A 0 ofNat(n) = ofNat(n) :=
  of_natCast A n

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

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

Разделы

Аффилиация

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