repsFintype — Mathlib

English

There is a finite type structure on the set reps(m) of representatives for determinant m.

Русский

У множества reps(m) имеется структура конечного типа как множества представителей.

LaTeX

$$Fintype (reps(m))$$

Lean4

noncomputable instance repsFintype (k : ℤ) : Fintype (reps k) :=
  by
  let H := Finset.Icc (-|k|) |k|
  let H4 := Fin 2 → Fin 2 → H
  apply Fintype.ofInjective (β := H4) (f := fun M i j ↦ ⟨M.1.1 i j, reps_entries_le_m' M.2 i j⟩)
  intro M N h
  ext i j
  simpa only [Subtype.mk.injEq] using congrFun₂ h i j

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