instDivCoeOfSubgroupClass — Mathlib

English

If each S_i is a DivInvMonoid and each S_i is a subgroup, then the restricted product inherits division defined componentwise: (x / y)_i = x_i / y_i.

Русский

Если каждое S_i является делимым полем без нуля (DivInvMonoid) и каждое S_i образует подгруппу, то ограниченное произведение унаследует операцию деления по координатам: (x / y)_i = x_i / y_i.

LaTeX

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

Lean4

@[to_additive]
instance [Π i, DivInvMonoid (R i)] [∀ i, SubgroupClass (S i) (R i)] : Div (Πʳ i, [R i, B i]_[𝓕]) where
  div x y := ⟨fun i ↦ x i / y i, y.2.mp (x.2.mono fun _ ↦ div_mem)⟩

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