div_apply — Mathlib

English

The coordinatewise division law holds for x, y in the restricted product: (x / y) i = x i / y i for every i.

Русский

Пусть x, y принадлежат ограниченному произведению; тогда выполняется (x / y)_i = x_i / y_i для каждого i.

LaTeX

$$$ (x / y)_i = x_i / y_i \quad (\forall i). $$$

Lean4

@[to_additive (attr := simp)]
theorem div_apply [Π i, DivInvMonoid (R i)] [∀ i, SubgroupClass (S i) (R i)] (x y : Πʳ i, [R i, B i]_[𝓕]) (i : ι) :
    (x / y) i = x i / y i :=
  rfl

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