No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
72@[simp] theorem add_apply (u v : F2Power D) (i : Fin D) :
73 (u + v) i = xor (u i) (v i) := rfl
proof body
Term-mode proof.
74
75/-- Negation in characteristic 2 is the identity. -/
76instance : Neg (F2Power D) := ⟨fun v => v⟩
77
depends on (7)
Lean names referenced from this declaration's body.
-
F2Power
in IndisputableMonolith.Algebra.F2Power
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use