OAI/Analysis/AffineBernstein/RadialAdjugateGL.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.radial_adjugate_exists_scalar line 21

   Source comment

   The cofactor tensor of a symmetric matrix with any nonzero radial null vector is a scalar multiple of its radial outer product. No rank or positive definiteness assumption is needed, including an empty transverse block.

   lemma radial_adjugate_exists_scalar {K : Matrix (ι ⊕ Unit) (ι ⊕ Unit) ℝ}
       (hK : K.IsSymm) {v : ι ⊕ Unit → ℝ} (hv : v ≠ 0) (hz : K *ᵥ v = 0) :
       ∃ c : ℝ, K.adjugate = c • Matrix.vecMulVec v v := by
   …

2. lemma OAI.AffineBernstein.adjugate_congruence_radial line 53
3. lemma OAI.AffineBernstein.adjugate_congruence_trace_radial line 66