tprod_pi_single — Mathlib

English

For any β with decidable equality and any a ∈ α, the tprod over b′ of Pi.mulSingle b a b′ equals a.

Русский

Для любого β с разрешимым равенством и любого a ∈ α, т-продукт по b′ от Pi.mulSingle b a b′ равен a.

LaTeX

$$$\\forall {\\beta} [DecidableEq β], \\; (tprod (\\lambda b', Pi.mulSingle b a b') ) = a$$$

Lean4

@[to_additive (attr := simp)]
theorem tprod_pi_single [DecidableEq β] (b : β) (a : α) : ∏' b', Pi.mulSingle b a b' = a :=
  by
  rw [tprod_eq_mulSingle b]
  · simp
  · intro b' hb'; simp [hb']

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