Shear.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DiagonalZonotope.shear line 14
Source documentation
The determinant-one shear that supplies the linear part of a facet extrusion.
```
def shear (i : ι) : (ι → ℝ) →ₗ[ℝ] (ι → ℝ) where
…
```
lemma OAI.DiagonalZonotope.shear_matrix line 27
theorem OAI.DiagonalZonotope.shear_det line 42
Source documentation
No absolute determinant factor is lost in the extrusion parameterization.
```
theorem shear_det (i : ι) : LinearMap.det (shear i) = 1 := by
…
```
Mentions: OAI.DiagonalZonotope.shear
lemma OAI.DiagonalZonotope.extrusionMap_eq line 46