OAI/Combinatorics/HadwigerCounterexample/ResponseAnnihilators.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.dotL line 14
2. theorem OAI.HadwigerCounterexample.dotL_surj line 20
3. theorem OAI.HadwigerCounterexample.protection_test line 36
4. theorem OAI.HadwigerCounterexample.Volley.mark_test line 84
5. theorem OAI.HadwigerCounterexample.Volley.ev_mput line 122
6. theorem OAI.HadwigerCounterexample.Volley.mark_diag line 129

   Source documentation

   Diagnostic for the two quotients by one affine ray.

   private theorem mark_diag {J : Type} [Fintype J] (Z : Mat (Option J) (Option J))
       (hZ : Zᵀ = Z) (hd : ∀ i,Z i i=Z none i) (v : Vec (Option J))
       (hv : v none=1) (he : ∀ φ, dotProduct φ v = 0 → ∀ ψ, dotProduct ψ v = 0 →
         evmat Z φ ψ=0) :
       Z = (Z none none) • vecMulVec v v := by
   …

   Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.evmat

7. theorem OAI.HadwigerCounterexample.Volley.mark_atom line 161