single — Mathlib

English

Under a suitable finite type and choice of index, CompleteOrthogonalIdempotents e can be realized as Pi.single-based family.

Русский

При подходящем конечном типе и выборе индексов CompleteOrthogonalIdempotents e можно реализовать как семью на основе Pi.single.

LaTeX

$$CompleteOrthogonalIdempotents e$$

Lean4

theorem single {I : Type*} [Fintype I] [DecidableEq I] (R : I → Type*) [∀ i, Semiring (R i)] :
    CompleteOrthogonalIdempotents (Pi.single (M := R) · 1) :=
  by
  refine ⟨⟨by simp [IsIdempotentElem, ← Pi.single_mul], ?_⟩, Finset.univ_sum_single 1⟩
  intro i j hij
  ext k
  by_cases hi : i = k
  · subst hi; simp [hij]
  · simp [hi]

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