`F2Power`

definition

show as: view math explainer →

module: IndisputableMonolith.Algebra.F2Power
domain: Algebra
line: 49 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Algebra.F2Power on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  46
  47/-- The elementary abelian 2-group of rank `D`, modeled as
  48    `Fin D → Bool` with pointwise XOR. -/
  49def F2Power (D : ℕ) : Type := Fin D → Bool
  50
  51namespace F2Power
  52
  53variable {D : ℕ}
  54
  55instance : DecidableEq (F2Power D) := by
  56  unfold F2Power; infer_instance
  57
  58instance : Fintype (F2Power D) := by
  59  unfold F2Power; infer_instance
  60
  61instance : Inhabited (F2Power D) := by
  62  unfold F2Power; infer_instance
  63
  64/-- The zero element: all coordinates `false`. -/
  65instance : Zero (F2Power D) := ⟨fun _ => false⟩
  66
  67@[simp] theorem zero_apply (i : Fin D) : (0 : F2Power D) i = false := rfl
  68
  69/-- Pointwise XOR. -/
  70instance : Add (F2Power D) := ⟨fun u v => fun i => xor (u i) (v i)⟩
  71
  72@[simp] theorem add_apply (u v : F2Power D) (i : Fin D) :
  73    (u + v) i = xor (u i) (v i) := rfl
  74
  75/-- Negation in characteristic 2 is the identity. -/
  76instance : Neg (F2Power D) := ⟨fun v => v⟩
  77
  78@[simp] theorem neg_eq_self (v : F2Power D) : -v = v := rfl
  79

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.