evenOdd_isCompl — Mathlib

English

The two graded components evenOdd(Q,0) and evenOdd(Q,1) form a complementary pair in the ambient graded structure.

Русский

Две градуированные компоненты evenOdd(Q,0) и evenOdd(Q,1) образуют комплементарную пару в общей градуированной структуре.

LaTeX

$$IsCompl (evenOdd(Q,0)) (evenOdd(Q,1))$$

Lean4

theorem evenOdd_isCompl : IsCompl (evenOdd Q 0) (evenOdd Q 1) :=
  (DirectSum.Decomposition.isInternal (evenOdd Q)).isCompl zero_ne_one <|
    by
    have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl
    simpa using congr_arg ((↑) : Finset (ZMod 2) → Set (ZMod 2)) this

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