operations): add missing `@[elab_as_eliminator]` on recursors (#12440)

Commit

4 years ago

chore(algebra/algebra/operations): add missing `@[elab_as_eliminator]` on recursors (#12440) `refine submodule.pow_induction_on' _ _ _ _ h` struggles without this attribute

Author

eric-wieser

Parents

4a416bc2

mathlib a7217000 - chore(algebra/algebra/operations): add missing `@[elab_as_eliminator]` on recursors (#12440)

mathlib
a7217000 - chore(algebra/algebra/operations): add missing `@[elab_as_eliminator]` on recursors (#12440)