English
For any f: M →* N →* P, f(1, n) = 1 for all n; i.e., the map sends the identity to the identity on the second argument.
Русский
Для любого f: M →* N →* P выполняется f(1,n)=1; т.е. отображение отправляет единицу в единицу во втором аргументе.
LaTeX
$$$\forall f:\,M\to^*N\to^*P,\; f\,1\,n=1$$$
Lean4
/-- `flip` arguments of `f : M →* N →* P` -/
@[to_additive /-- `flip` arguments of `f : M →+ N →+ P` -/
]
def flip {mM : MulOneClass M} {mN : MulOneClass N} {mP : CommMonoid P} (f : M →* N →* P) : N →* M →* P
where
toFun
y :=
{ toFun := fun x => f x y, map_one' := by simp [f.map_one, one_apply],
map_mul' := fun x₁ x₂ => by simp [f.map_mul, mul_apply] }
map_one' := ext fun x => (f x).map_one
map_mul' y₁ y₂ := ext fun x => (f x).map_mul y₁ y₂
