sign_mul — Mathlib

English

For all x,y ∈ α in a linearly ordered ring, sign(xy) = sign x · sign y.

Русский

Для любых x, y ∈ α в упорядоченном кольце знак произведения равен произведению знаков: sign(xy) = sign(x)·sign(y).

LaTeX

$$$\operatorname{sign}(xy) = \operatorname{sign}(x) \operatorname{sign}(y)$$$

Lean4

theorem sign_mul (x y : α) : sign (x * y) = sign x * sign y := by
  rcases lt_trichotomy x 0 with (hx | hx | hx) <;> rcases lt_trichotomy y 0 with (hy | hy | hy) <;>
    simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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