map_one₂ — Mathlib

English

The flip construction is involutive in the sense that applying flip twice yields the original structure, i.e., f.flip.flip = f.

Русский

Операция разворота (flip) обратно восстанавливает исходную структуру при повторном применении.

LaTeX

$$$\text{flip}(\text{flip}(f))=f$$$

Lean4

@[to_additive]
theorem map_one₂ {_ : MulOneClass M} {_ : MulOneClass N} {_ : CommMonoid P} (f : M →* N →* P) (n : N) : f 1 n = 1 :=
  (flip f n).map_one

Похожие утверждения