English
Push forward a MonoidWithZero along a surjective function: given f: M0 → M0' surjective, one obtains a MonoidWithZero on M0'.
Русский
Сдвиг моноида с нулём вдоль сюръективной функции: есть f: M0 → M0', сюръективна, тогда получается MonoidWithZero на M0'.
LaTeX
$$$\\text{MonoidWithZero } M_0' = \\text{ pushforward along } f$$$
Lean4
/-- Push forward a `MonoidWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [MonoidWithZero M₀] (f : M₀ → M₀')
(hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
(npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) : MonoidWithZero M₀' :=
{ hf.monoid f one mul npow, hf.mulZeroClass f zero mul with }
