def definition def or abbrev

`tPulledConnection`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  27noncomputable def tPulledConnection {n : ℕ} (x : Vec n) (i j k : Fin n) : ℝ :=

Definition body.

  28  if i = j ∧ j = k then -(x i)⁻¹ else 0
  29
  30/-- Projective equivalence to the zero connection. -/

From the project-wide theorem graph. These declarations reference this one in their body.

not_projectivelyEquivalentToZeroAt_tPulledConnection in IndisputableMonolith.Cost.Ndim.Connections decl_use
projectivelyEquivalent_one_dim in IndisputableMonolith.Cost.Ndim.Connections decl_use
tPulledConnection_diag in IndisputableMonolith.Cost.Ndim.Connections decl_use
tPulledConnection_offDiag in IndisputableMonolith.Cost.Ndim.Connections decl_use

Lean names referenced from this declaration's body.