instNatCastLex

Mathlib.Data.Nat.Cast.Synonym

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

English

The dual equivalence preserves nat casts: (ofDual n.cast) = n.cast in the dual.

Русский

Эквививалентность двойственности сохраняет nat cast: (ofDual n.cast) = n.cast в двойственном порядке.

LaTeX

$$$ (\mathrm{ofDual}\, (n.cast)) = n.cast $$$

Lean4

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

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

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

Разделы

Аффилиация

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