English
Let F be a monoid and c: F → M → M satisfy c(1) = id and c(f g) = c f ∘ c g; then for any f ∈ F and n ∈ N, c(f^n) = (c f)^[n].
Русский
Пусть F — моноид, и функция c с условием c(1)=id и c(f g)=c f ∘ c g; тогда для любого f ∈ F и n ∈ N имеет место c(f^n) = (c f)^[n].
LaTeX
$${F : Type*} [Monoid F] (c : F → M → M) (h1 : c 1 = id) (hmul : ∀ f g, c (f * g) = c f ∘ c g) (f : F) : ∀ n, c (f ^ n) = (c f)^[n]$$
Lean4
/-- If a binary function from a type equipped with a total relation `r` to a monoid is
anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
(i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
We allow restricting to a subset specified by a predicate `p`. -/
@[to_additive additive_of_isTotal /-- If a binary function from a type equipped with a total
relation `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in
order to show it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and
`r b c` are satisfied. We allow restricting to a subset specified by a predicate `p`. -/
]
theorem multiplicative_of_isTotal (p : α → Prop) (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1)
(hmul : ∀ {a b c}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) {a b c : α} (pa : p a) (pb : p b)
(pc : p c) : f a c = f a b * f b c :=
by
apply multiplicative_of_symmetric_of_isTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
· simp_rw [and_imp]; exact @hswap
· exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
