English
Pull back a MonoidWithZero along an injective function: given f: M0' → M0 with appropriate structure, one obtains a MonoidWithZero on M0'.
Русский
Переносим MonoidWithZero вдоль инъекции: дано f: M0' → M0 с необходимыми структурами, получается MonoidWithZero на M0'.
LaTeX
$$$\\text{MonoidWithZero } M_0' = \\text{ pullback along } f$$$
Lean4
/-- Pull back a `MonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' ℕ] [MonoidWithZero 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) : MonoidWithZero M₀' :=
{ hf.monoid f one mul npow, hf.mulZeroClass f zero mul with }
