commMonoidWithZero — Mathlib

English

Pull back a CommMonoidWithZero along an injective function: the structure is inherited on the domain.

Русский

Переносим CommMonoidWithZero вдоль инъекции: структура наследуется исходным доменом.

LaTeX

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

Lean4

/-- Pull back a `CommMonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev commMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [CommMonoidWithZero M₀] (f : M₀' → M₀)
    (hf : Injective 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 }

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