ofDual_ofNat — Mathlib

English

The dual-to-original embedding preserves nat casting: for any n, (toDual(ofNat n)) = ofNat n in the dual setting.

Русский

Преобразование обратно в исходный порядок сохраняет nat casting: for all n, (toDual(ofNat n)) = ofNat n.

LaTeX

$$$ toDual\big((\mathrm{ofNat}(n) : \alpha^{\mathrm{opp}})\big) = \mathrm{ofNat}(n) $$$

Lean4

@[simp]
theorem ofDual_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] : (ofDual (ofNat(n) : αᵒᵈ)) = ofNat(n) :=
  rfl

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