sign_eq_sign

Mathlib.Data.Sign.Defs

URI: https://scilib.ai/kg/mathlib#Int.sign_eq_sign

English

For every integer n, Int.sign n = SignType.sign n.

Русский

Для каждого целого числа n выполняется Int.sign n = SignType.sign n.

LaTeX

$$$ \forall n \in \mathbb{Z},\ \operatorname{Int.sign}(n) = \operatorname{SignType.sign}(n). $$$

Lean4

theorem sign_eq_sign (n : ℤ) : Int.sign n = SignType.sign n := by
  obtain (n | _) | _ := n <;> simp [sign, negSucc_lt_zero]

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

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

Разделы

Аффилиация

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