English
Push forward a LeftDistribClass structure along a surjective map from R to S: if R has a LeftDistribClass and a compatible ring structure, then S inherits a LeftDistribClass via the surjection.
Русский
Перенос левого распределительного класса по сюръективному отображению: если R обладает LeftDistribClass и совместной структурой кольца, то S наследует LeftDistribClass через отображение.
LaTeX
$$$\\text{LeftDistribClass } S \\text{ with } (left\_distrib) \\;\\equiv\\; \\forall x,y,z,\\; x\\cdot_S(y+z)=xy+xz,$$$
Lean4
/-- Pushforward a `LeftDistribClass` instance along a surjective function. -/
theorem leftDistribClass [Mul R] [Add R] [LeftDistribClass R] (add : ∀ x y, f (x + y) = f x + f y)
(mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass S where
left_distrib := hf.forall₃.2 fun x y z => by simp only [← add, ← mul, left_distrib]
