English
If R is a distributive algebraic structure, then the germ construction l.Germ R inherits a distributive structure: multiplication distributes over addition on the germ level, i.e., for all germs a, b, c in l.Germ R, a · (b + c) = a · b + a · c and (b + c) · a = b · a + c · a.
Русский
Если R обладает распределённой структурой (распределение умножения по сложению), то конструирование Герма по фильтру l наследует распределённую структуру: умножение распределяется по сложению на уровне Герма, т.е. для любых Герма a, b, c верно a · (b + c) = a · b + a · c и (b + c) · a = b · a + c · a.
LaTeX
$$$\text{Distrib}(\mathrm{Germ}\,l\,R)$$$
Lean4
instance instDistrib [Distrib R] : Distrib (Germ l R)
where
left_distrib a b c := Quotient.inductionOn₃' a b c fun _ _ _ ↦ congrArg ofFun <| left_distrib ..
right_distrib a b c := Quotient.inductionOn₃' a b c fun _ _ _ ↦ congrArg ofFun <| right_distrib ..
