eval — Mathlib

English

For l : Profinite.NobelingProof.Products I, eval C l = List.map (e C) l.val . prod.

Русский

Для l ∈ Profinite.NobelingProof.Products I выполнено: eval C l = (List.map (e C) l.val).prod.

LaTeX

$$$$ \\mathrm{eval}\\, C\\, l = \\Big(\\mathrm{List}.\\mathrm{map}(\\mathrm{e}\\, C)\\, l.\\text{val}\\Big).\\mathrm{prod}. $$$$

Lean4

/-- The evaluation `e C i₁ ··· e C iᵣ : C → ℤ` of a formal product `[i₁, i₂, ..., iᵣ]`. -/
def eval (l : Products I) :=
  (l.1.map (e C)).prod

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