English
If S is a submonoid of M, and l is a list of elements of S, then the product in M of the l equals the product of the coerced elements in M.
Русский
Если S — подмоном M, и l — список элементов из S, то произведение в M элементов списка равно произведению их образов в M.
LaTeX
$$$\\operatorname{prod}_{l} \\;(l) = \\operatorname{prod}_{l} \\; (\\uparrow l)$$$
Lean4
/-- Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid.
Then `MonoidHom.ofClosureEqTopLeft` defines a monoid homomorphism from `M` asking for
a proof of `f (x * y) = f x * f y` only for `x ∈ s`. -/
@[to_additive /-- Let `s` be a subset of an additive monoid `M` such that the closure of `s` is
the whole monoid. Then `AddMonoidHom.ofClosureEqTopLeft` defines an additive monoid
homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `x ∈ s`. -/
]
def ofClosureMEqTopLeft {M N} [Monoid M] [Monoid N] {s : Set M} (f : M → N) (hs : closure s = ⊤) (h1 : f 1 = 1)
(hmul : ∀ x ∈ s, ∀ (y), f (x * y) = f x * f y) : M →* N
where
toFun := f
map_one' := h1
map_mul'
x :=
dense_induction (motive := _) _ hs hmul (fun y => by rw [one_mul, h1, one_mul])
(fun a b ha hb y => by rw [mul_assoc, ha, ha, hb, mul_assoc]) x
