[Merged by Bors] - chore: register TensorProduct
with induction_eliminator
#14204
Closed
eric-wieser wants to merge 2 commits intomasterfrom eric-wieser/TensorProduct-induction
TensorProduct
with induction_eliminator
#14204