Wikipedia · textbook · AMS 20 37
mediumknown result, no worker yet
Gottschalk's surjunctivity conjecture
Theorem · isSurjunctive_of_finite
Every finite group is surjunctive. This is a classical result: an injective endomorphism of a finite set is surjective.
Formal statement · Lean 4.lean
theorem isSurjunctive_of_finite (G : Type) [Group G] [Finite G] :
IsSurjunctive G := by
sorryProof. sorry
Nobody has tried yet.