pith. machine review for the scientific record. sign in
lemma

consistent_zero

proved
show as:
view math explainer →
module
IndisputableMonolith.RecogSpec.Anchors
domain
RecogSpec
line
16 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogSpec.Anchors on GitHub at line 16.

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

formal source

  13
  14namespace Anchors
  15
  16@[simp] lemma consistent_zero (A : Anchors) : A.a1 = 0 → A.a2 = 0 :=
  17  A.consistent
  18
  19end Anchors
  20
  21end RecogSpec
  22end IndisputableMonolith

papers checked against this theorem

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