English
The collection of all R-linear automorphisms of M forms a group under composition, with the identity map as the unit and inverse given by the inverse automorphism.
Русский
Множество всех R-линейных автоморфизмов пространства M образует группу под операцией композиции; единицей является тождественный отображение, а обратное к f — обратное отображение f.
LaTeX
$$$ \mathrm{Aut}_R(M) \text{ is a group under composition with } f \cdot g = f \circ g, \ 1 = \mathrm{id}_M, \ f^{-1} = f^{-1}. $$$
Lean4
instance automorphismGroup : Group (M ≃ₗ[R] M)
where
mul f g := g.trans f
one := LinearEquiv.refl R M
inv f := f.symm
mul_assoc _ _ _ := rfl
mul_one _ := ext fun _ ↦ rfl
one_mul _ := ext fun _ ↦ rfl
inv_mul_cancel f := ext <| f.left_inv
