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: Dec 21 2024 at 16:20 UTC