mulSingle_div — Mathlib

English

Let (f i) be a family of groups indexed by I. For every i in I and every x, y in f i, the injection mulSingle i sends division componentwise, i.e. mulSingle i (x / y) = mulSingle i x / mulSingle i y.

Русский

Пусть для каждого i∈I задана группа f i. Тогда вложение mulSingle i: f i → ∀ i, f i сохраняет деление по координатам: mulSingle i (x / y) = mulSingle i x / mulSingle i y.

LaTeX

$$$\mathrm{mulSingle}_i(x/y) = \mathrm{mulSingle}_i x / \mathrm{mulSingle}_i y$$$

Lean4

@[to_additive]
theorem mulSingle_div [∀ i, Group <| f i] (i : I) (x y : f i) : mulSingle i (x / y) = mulSingle i x / mulSingle i y :=
  (MonoidHom.mulSingle f i).map_div x y

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