English
The inverse-preserving variants of mulIndicator yield a consistent monoid-homomorphism structure; the inverse version holds componentwise.
Русский
Версии с сохранением обратного для mulIndicator образуют корректную структуру гомоморфизма моноидов; обратное сохраняется по компонентам.
LaTeX
$$$$ \\forall s:\\ Set\\alpha, f:\\alpha \\to G,\\ (mulIndicator s f)^{-1} = mulIndicator s f^{-1} $$$$
Lean4
/-- A type endowed with `1` and `*` is a monoid, if it admits an injective map that preserves `1`
and `*` to a monoid. See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and `+` is an additive monoid, if it admits an
injective map that preserves `0` and `+` to an additive monoid. See note
[reducible non-instances]. -/
]
protected abbrev monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
(mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁ :=
{ hf.mulOneClass f one mul, hf.semigroup f mul with npow := fun n x => x ^ n,
npow_zero := fun x => hf <| by rw [npow, one, pow_zero],
npow_succ := fun n x => hf <| by rw [npow, pow_succ, mul, npow] }
