sign_intCast — Mathlib

English

For any integer n, the sign of n as an α-element coincides with the sign of n in SignType: sign(n : α) = sign n.

Русский

Для любого целого числа n знак числа n, как элемент α, совпадает со знаком n в SignType: sign(n : α) = sign n.

LaTeX

$$$\operatorname{sign}(n : \alpha) = \operatorname{sign} n$$$

Lean4

@[simp]
theorem sign_intCast {α : Type*} [Ring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] [DecidableLT α] (n : ℤ) :
    sign (n : α) = sign n := by simp only [sign_apply, Int.cast_pos, Int.cast_lt_zero]

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