English
If G is a group, then the space of C^n-maps inherits a group structure under pointwise multiplication, including the inverse, so it is a group under the natural pointwise operation.
Русский
Если G — группа, то пространство C^n-отображений образует группу под точечным умножением (включая обратное).
LaTeX
$$$\text{If }G\text{ is a group, then }C^n(I,N;I',G)\text{ is a group under }(f\cdot g)(x)=f(x)g(x).$$$
Lean4
@[to_additive]
instance group {G : Type*} [Group G] [TopologicalSpace G] [ChartedSpace H' G] [LieGroup I' n G] :
Group C^n⟮I, N; I', G⟯ :=
{ ContMDiffMap.monoid with
inv := fun f => ⟨fun x => (f x)⁻¹, f.contMDiff.inv⟩
inv_mul_cancel := fun a => by ext; exact inv_mul_cancel _
div := fun f g => ⟨f / g, f.contMDiff.div g.contMDiff⟩
div_eq_mul_inv := fun f g => by ext; exact div_eq_mul_inv _ _ }
