toDual_natCast

Mathlib.Data.Nat.Cast.Synonym

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

English

For any α with a NatCast, the dual-number embedding sends natural numbers to themselves in the dual order.

Русский

Для любого типа α с NatCast двойственный порядок сохраняет натуральные числа независимo.

LaTeX

$$$ \text{toDual}(n : \alpha) = n $$$

Lean4

@[simp]
theorem toDual_natCast [NatCast α] (n : ℕ) : toDual (n : α) = n :=
  rfl

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

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

Разделы

Аффилиация

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