English
Any finite group G of universe u is equivalent to some finite group G' in universe v; i.e., there exists a finite group G' and a MulEquiv G ≃* G'.
Русский
Любая конечная группа G во вселенной u эквивалентна некоторой конечной группе G' во вселенной v; то есть существует мул-эквивалентность G ≃* G'.
LaTeX
$$$\exists G',\ (\text{Group } G')\land (\text{Fintype } G')\land (G \simeq^* G')$$$
Lean4
/-- Any finite group in universe `u` is equivalent to some finite group in universe `v`. -/
@[to_additive /-- Any finite group in universe `u` is equivalent to some finite group in universe `v`. -/
]
theorem exists_type_univ_nonempty_mulEquiv.{u, v} (G : Type u) [Group G] [Finite G] :
∃ (G' : Type v) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G') :=
by
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
let f : Fin n ≃ ULift (Fin n) := Equiv.ulift.symm
let e : G ≃ ULift (Fin n) := e.trans f
letI groupH : Group (ULift (Fin n)) := e.symm.group
exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩
