instFintypeAddEquivInt — Mathlib

English

The structure of AddEquiv on integers is finite, with only two basic additive automorphisms: identity and negation.

Русский

Структура AddEquiv на множествах целых чисел конечна: два базовых автоморфизма — тождественный и отрицание.

LaTeX

$$$ \text{Finite}(\mathrm{AddEquiv}(\mathbb{Z}, \mathbb{Z})) \\text{(two elements: refl and neg)} $$$

Lean4

instance : Fintype (ℤ ≃+ ℤ)
    where
  elems := .cons (.neg _) ({.refl _}) (by simp [AddEquiv.ext_int_iff])
  complete x := by obtain rfl | rfl := Int.addEquiv_eq_refl_or_neg x <;> simp

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