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: Sep 11 2024 at 16:22 UTC