arithmetic): improve `enum_iso` def-eq (#15454)

Commit

3 years ago

chore(set_theory/ordinal/arithmetic): improve `enum_iso` def-eq (#15454) By not casing on the argument of `to_fun`, we get much a much nicer `apply` projection.

Author

vihdzp

Parents

2067c013

mathlib 09ff086c - chore(set_theory/ordinal/arithmetic): improve `enum_iso` def-eq (#15454)

mathlib
09ff086c - chore(set_theory/ordinal/arithmetic): improve `enum_iso` def-eq (#15454)