def NOF.eval {ι : Type u_1} {G : Type u_2} [AddCommGroup G] [DecidableEq G] [Fintype ι] (x : ι → G) : Bool

Equations

• NOF.eval x = (∑ i : ι, x i == 0)

@[simp]

theorem NOF.eval_eq_true {ι : Type u_1} {G : Type u_2} [AddCommGroup G] [DecidableEq G] [Fintype ι] {x : ι → G} : eval x = true ↔ ∑ i : ι, x i = 0

theorem NOF.trivial_of_isForbiddenPattern_of_isValid_eval {G : Type u_2} [AddCommGroup G] [DecidableEq G] {d : ℕ} [NeZero d] {P : Protocol G d} {t : ℕ} {B : List Bool} {a : ZMod d → ZMod d → G} (ha : IsForbiddenPattern a) (hP : P.IsValid eval t) (hE : ∀ (i : ZMod d), eval (a i) = true) (hB : ∀ (i : ZMod d), P.broadcast (a i) t = B) (i j : ZMod d) : a i = a j

def NOF.getBits (B : List Bool) (i d : ℕ) : List Bool

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NOF.Protocol.trivial {G : Type u_2} [AddCommGroup G] {d : ℕ} [Fintype G] (hd : 3 ≤ d) (F : (ZMod d → G) → Bool) : Protocol G d

Equations

• One or more equations did not get rendered due to their size.