pith. machine review for the scientific record. sign in
theorem proved tactic proof

not_projectivelyEquivalentToZeroAt_tPulledConnection

show as:
view Lean formalization →

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)

  59theorem not_projectivelyEquivalentToZeroAt_tPulledConnection {n : ℕ}
  60    (hn : 2 ≤ n) (x : Vec n) (hx : ∀ i : Fin n, x i ≠ 0) :
  61    ¬ ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by

proof body

Tactic-mode proof.

  62  let i0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hn⟩
  63  let i1 : Fin n := ⟨1, lt_of_lt_of_le (by decide : 1 < 2) hn⟩
  64  have hi01 : i0 ≠ i1 := by
  65    simp [i0, i1]
  66  intro hproj
  67  rcases hproj with ⟨ψ, hψ⟩
  68  have hpsi1 : ψ i1 = 0 := by
  69    have h := hψ i0 i0 i1
  70    simpa [eq_comm, delta, tPulledConnection, hi01] using h
  71  have hdiag : tPulledConnection x i1 i1 i1 = delta i1 i1 * ψ i1 + delta i1 i1 * ψ i1 := by
  72    simpa using hψ i1 i1 i1
  73  have hxinv_zero : (x i1)⁻¹ = 0 := by
  74    have h' : -(x i1)⁻¹ = 0 := by
  75      simpa [delta, tPulledConnection, hpsi1] using hdiag
  76    exact neg_eq_zero.mp h'
  77  exact (inv_ne_zero (hx i1)) hxinv_zero
  78
  79end Ndim
  80end Cost
  81end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.