English
Push forward a RightDistribClass structure along a surjective map: if R has RightDistribClass, then S inherits it via the surjection.
Русский
Перенос правого распределительного класса по сюръекции: если R обладает RightDistribClass, то S получает его через сюръекцию.
LaTeX
$$$\\text{RightDistribClass } S \\text{ with } (right\\_distrib) \\;\\equiv\\; \\forall x,y,z,\\; (x+ y)\\cdot_S z = xz+yz,$$$
Lean4
/-- Pushforward a `RightDistribClass` instance along a surjective 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 := hf.forall₃.2 fun x y z => by simp only [← add, ← mul, right_distrib]
