def
definition
def or abbrev
ProjectivelyEquivalentToZeroAt
show as:
view Lean formalization →
formal statement (Lean)
31def ProjectivelyEquivalentToZeroAt {n : ℕ}
32 (Γ : Fin n → Fin n → Fin n → ℝ) : Prop :=
proof body
Definition body.
33 ∃ ψ : Vec n, ∀ i j k : Fin n,
34 Γ i j k = delta i j * ψ k + delta i k * ψ j
35