English
Given an additive commutative group A and a ring morphism R →+* End A, mkOfSMul' φ provides a type-equivalent copy of A, over which one can later define an R-module structure.
Русский
Пусть A — абелева группа. При наличии кольцевого морфизма R →+* End A объект mkOfSMul' φ представляет собой тот же набор элементов, что и A, на котором впоследствии можно определить структуру R-модуля.
LaTeX
$$$\text{mkOfSMul' } \phi \text{ это просто копия } A\text{ как множество/объект, на котором можно определить структуру модуля } R$.$$
Lean4
/-- Given `A : AddCommGrpCat` and a ring morphism `R →+* End A`, this is a type synonym
for `A`, on which we shall define a structure of `R`-module. -/
@[nolint unusedArguments]
def mkOfSMul' {A : AddCommGrpCat} (_ : R →+* End A) :=
A
