English
If p is a predicate on α and IsTotal α r, then the multiplicative property can be extended from pairwise to triples under p, using a functional f: α → α → β into a Monoid.
Русский
Если p — предикат на α и IsTotal α r, то умножаемость может распространяться на тройки через функцию f: α → α → β в мономиед, при условии pa, pb, pc.
LaTeX
$$(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}, p a → p b → p c → f a c = f a b * f b c$$
Lean4
/-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`. -/
@[to_additive]
theorem hom_coe_pow {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]
| 0 => by
rw [pow_zero, h1]
rfl
| n + 1 => by rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]
