α β : Type u
a b c : Cardinal
⊢ a ^ (c * b) = (a ^ b) ^ c
α β : Type u
a b c : Cardinal
⊢ a ^ (b * c) = (a ^ b) ^ c
rw [mul_comm b c]
no goals
α β : Type u
a b c : Cardinal
⊢ a ^ (c * b) = (a ^ b) ^ c
exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α