cancelCommMonoidWithZero — Mathlib

English

Pull back a CancelCommMonoidWithZero along an injective function; the domain inherits cancellative properties.

Русский

Переносим CancelCommMonoidWithZero вдоль инъекции; домен наследует свойства отменяемости и нуля.

LaTeX

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

Lean4

/-- Pull back a `CancelCommMonoidWithZero` along an injective function.
See note [reducible non-instances]. -/
protected abbrev cancelCommMonoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow 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) :
    CancelCommMonoidWithZero M₀' :=
  { hf.commMonoidWithZero f zero one mul npow, hf.cancelMonoidWithZero f zero one mul npow with }

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