instFloorRingInt — Mathlib

English

For any a,b ∈ α and n ∈ ℤ, if n ≠ 0, a^n = -b^n iff a = -b and Odd n.

Русский

Для любых a,b ∈ α и n ∈ ℤ, n ≠ 0: a^n = -b^n эквивалентно a = -b и нечётно.

LaTeX

$$$\forall a,b \in \alpha, \forall n \in \mathbb{Z}, n \ne 0 \Rightarrow a^{n} = -b^{n} \iff a = -b \land \mathrm{Odd}(n)$$$

Lean4

instance : FloorRing ℤ where
  floor := id
  ceil := id
  gc_coe_floor a b := by rw [Int.cast_id, id_def]
  gc_ceil_coe a b := by rw [Int.cast_id, id_def]

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