It generally has some nicer properties. It would make sense to define to_nat
in terms of to_nat_on
and inherit all the nice properties.
great answer, thank you
Robert Soeldner has marked this topic as resolved.
Last updated: Feb 01 2025 at 20:19 UTC