commMonoidWithZero — Mathlib

English

Push forward a CommMonoidWithZero along a surjective function.

Русский

Пушфорвард коммутативного моноида с нулём по сюръективной функции.

LaTeX

$$$\\text{CommMonoidWithZero } M_0' = \\text{ pushforward along } f$$$

Lean4

/-- Push forward a `CommMonoidWithZero` along a surjective function.
See note [reducible non-instances]. -/
protected abbrev commMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [CommMonoidWithZero 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) : CommMonoidWithZero M₀' :=
  { hf.commMonoid f one mul npow, hf.mulZeroClass f zero mul with }

Похожие утверждения