English
If T has a unique element, the free abelian group on T is canonically isomorphic to the integers ℤ.
Русский
Если у типа T ровно один элемент, то свободная абелеева группа на T канонически изоморфна группе целых чисел ℤ.
LaTeX
$$$ \\mathrm{FreeAbelianGroup}(T) \\cong_+ \\mathbb{Z} $$$
Lean4
/-- The free abelian group on a type with one term is isomorphic to `ℤ`. -/
def uniqueEquiv (T : Type*) [Unique T] : FreeAbelianGroup T ≃+ ℤ
where
toFun := FreeAbelianGroup.lift fun _ ↦ (1 : ℤ)
invFun n := n • of Inhabited.default
left_inv
z :=
FreeAbelianGroup.induction_on z (by simp only [zero_smul, AddMonoidHom.map_zero])
(Unique.forall_iff.2 <| by simp only [one_smul, lift_apply_of]) (Unique.forall_iff.2 <| by simp) fun x y hx hy ↦
by
simp only [AddMonoidHom.map_add, add_smul] at *
rw [hx, hy]
right_inv
n := by
rw [AddMonoidHom.map_zsmul, lift_apply_of]
exact zsmul_int_one n
map_add' := AddMonoidHom.map_add _
