instAddCommMonoidWithOneLex

Mathlib.Data.Nat.Cast.Synonym

URI: https://scilib.ai/kg/mathlib#instAddCommMonoidWithOneLex

English

The Lex embedding sends OfNat(n) to the corresponding OfNat in the Lex-augmented type: toLex(ofNat n) = OfNat.ofNat n.

Русский

In Lex-структуре toLex(ofNat n) = OfNat.ofNat n.

LaTeX

$$$ toLex(\mathrm{ofNat}(n) : \mathrm{Lex}\, \alpha) = \mathrm{OfNat}.\mathrm{ofNat}\, n $$$

Lean4

instance [h : AddCommMonoidWithOne α] : AddCommMonoidWithOne (Lex α) :=
  h

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

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

Разделы

Аффилиация

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