mk_ofNat

Mathlib.Topology.Algebra.SeparationQuotient.Basic

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.mk_ofNat

English

If n ≥ 2, mk(ofNat(n)) = OfNat.ofNat(n) in SeparationQuotient.

Русский

Если n≥2, то mk(ofNat(n)) = OfNat.ofNat(n) в SeparationQuotient.

LaTeX

$$$mk\left(\mathrm{ofNat}(n)\right)=\mathrm{OfNat.ofNat}(n)$$$

Lean4

@[simp]
theorem mk_ofNat [NatCast R] (n : ℕ) [n.AtLeastTwo] : mk (ofNat(n) : R) = OfNat.ofNat n :=
  rfl

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

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

Разделы

Аффилиация

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