ImmBidegree.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.imm_mem_bidegreeSubmodule line 12

Source documentation

With a layerwise partition, IMM is already in the selected bidegree.

theorem imm_mem_bidegreeSubmodule (K : Type*) [CommSemiring K] (n : ℕ)
    (side : Fin n → Bool) :
    imm K n ∈ bidegreeSubmodule (fun x => side x.1)
      (Finset.univ.filter (fun t => side t = true)).card
      (Finset.univ.filter (fun t => side t = false)).card := by
…

Mentions: OAI.Problem335.imm, OAI.Problem335.bidegreeSubmodule

theorem OAI.Problem335.bidegreeComponent_imm line 35

Source documentation

A bidegree projection does not change IMM when the selected index is its layer count.

theorem bidegreeComponent_imm (K : Type*) [CommSemiring K] (n : ℕ)
    (side : Fin n → Bool) :
    bidegreeComponent (fun x => side x.1)
      (Finset.univ.filter (fun t => side t = true)).card
      (Finset.univ.filter (fun t => side t = false)).card (imm K n) = imm K n :=
…

Mentions: OAI.Problem335.bidegreeComponent, OAI.Problem335.imm