OAI/Geometry/Zonotope/Determinant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DiagonalZonotope.det_identity_updateCol_ones line 12

   Source documentation

   Replacing one identity column by the all-ones vector leaves determinant one.

   theorem det_identity_updateCol_ones (i : ι) :
       ((1 : Matrix ι ι R).updateCol i (fun _ => 1)).det = 1 := by
   …