English
A free group basis is naturally a FunLike object from the index set to the group, recording the images of generators.
Русский
База свободной группы естественно является объектом FunLike от индексного множества к группе, фиксируя образы генераторов.
LaTeX
$$$$ \\mathrm{FreeGroupBasis}_{ι} G \\text{ has a FunLike structure to map }ι \\to G. $$$$
Lean4
/-- A free group basis for `G` over `ι` is associated to a map `ι → G` recording the images of
the generators. -/
instance instFunLike : FunLike (FreeGroupBasis ι G) ι G
where
coe b := fun i ↦ b.repr.symm (FreeGroup.of i)
coe_injective' := by
rintro ⟨b⟩ ⟨b'⟩ hbb'
have H : (b.symm : FreeGroup ι →* G) = (b'.symm : FreeGroup ι →* G) := by ext i; exact congr_fun hbb' i
have : b.symm = b'.symm := by ext x; exact DFunLike.congr_fun H x
rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]
