rightDistribClass — Mathlib

English

Pull back a RightDistribClass structure along an injective map; the induced right distribution holds via the injection.

Русский

Предъявляем структуру RightDistribClass по инъекции; индуцированное право-распределение сохраняется через инъекцию.

LaTeX

$$Right distributivity on S is preserved: $f((x+y)\cdot z) = f(xz) + f(yz)$ for all suitable x,y,z.$$

Lean4

/-- Pullback a `RightDistribClass` instance along an injective function. -/
theorem rightDistribClass [Mul R] [Add R] [RightDistribClass R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass S where
  right_distrib x y z := hf <| by simp only [*, right_distrib]

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