fintype — Mathlib

English

For any function f: InfinitePlace(K) → α where α is a commutative monoid, the total product factors into real and complex parts: ∏ w f(w) = (∏ real w, f(w)) · (∏ complex w, f(w)).

Русский

Для произвольной функции f, считающей значения в коммутативном моноиде, произведение по всем местам распадается на произведения по реальным и комплексным местам.

LaTeX

$$$\forall f : \mathrm{InfinitePlace}(K) \to \alpha,\quad \prod_{w} f(w) = \left(\prod_{w \in \{ w : \mathrm{InfinitePlace}(K) \mid \mathrm{IsReal} w \}} f(w)\right) \left(\prod_{w \in \{ w : \mathrm{InfinitePlace}(K) \mid \mathrm{IsComplex} w \}} f(w)\right)$$$

Lean4

noncomputable instance fintype [NumberField K] : Fintype (InfinitePlace K) :=
  Set.fintypeRange _

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