@lkastner has added a first version of this in #2228. (Thank you!) If this needs to be moved/improved, people can find this first version in /src/PolyhedralGeometry/PolyhedralFan/properties.jl.

The definition for "unimodular matrix" I am familiar with is for square matrices only. So perhaps to get started on this, could you tell us what definition for non-square matrices you have in mind (ideally with a ref to a textbook definition, so it can be included in the docstring) ?

In principle I see no harm in having this, as long as we are very clear about what it means.

@JohnAAbbott has some code for determining if a square integer matrix (ZZMatrix) is unimodular. The code is almost ready to become a PR. Should the function be called is_unimodular? Currently its internal working name is different.

I am finalizing my impl of is_unimodular for square integer matrices.
Question: @lkastner is your code now in OSCAR -- the comment from @HereAround on 2023-04-14 suggests that it has now been included. But I cannot find it.
BTW here is a marginally faster/clearer version:

function _is_unimodular(M::ZZMatrix)
  return nrows(M) <= ncols(M) && all(is_equal(1), diagonal(snf(M)))
end

Do you have a reference for this definition? I am aware only of the definition abs(det(M)) == 1

Since I believe that my implementation should be usefully faster for square matrices, it would be nice to call my code when the input is square. We could make my code the main function, and make it delegate to your code for non-square matrices; or vice versa? What do you think?

I cannot find this function _is_unimodular in OSCAR neither. Maybe it was moved, but I cannot recall. Maybe @lkastner knows more?

For all it matters: In https://github.com/oscar-system/Oscar.jl/pull/2228/files a function _is_unimodular was added to /scr/PolyhedralGeometry/PolyhedralFan/properties.jl line 598ff:

function _is_unimodular(M::ZZMatrix)
  nrows(M) <= ncols(M) || return false
  n = nrows(M)
  return abs(det(snf(M)[:,1:n])) == 1
end

Another question for @lkastner : @fieker reports that non-square matrices which can be completed to a unimodular square matrix are known as saturated in some contexts (not sure if it also applies to a square matrix). Would the function name is_saturated for the function in your original post be OK?

The function _is_unimodular was deleted in c4633ce, apparently it was needed anymore, since star_subdivision now works in a more general case?

@JohnAAbbott I am fine with having is_saturated, maybe you could mention unimodular in the docs such that I will be able to find it? Since the workaround is gone there is no urgency.