mathlib

1483eca1 - feat(algebra/algebra/operations): add right induction principles for power membership (#14219)

feat(algebra/algebra/operations): add right induction principles for power membership (#14219) We already had the left-induction principles. There's probably some clever trick to get these via `mul_opposite`, but I'm not sure if it's worth the effort.