Commit 2024-09-17 23:02 19286096

View on Github →

chore(SetTheory/Cardinal/Basic): inline mul_comm into instance (#16851) We also make the arguments of power_zero, power_one, and power_add explicit.

Estimated changes

modified theorem Cardinal.power_add
modified theorem Cardinal.power_one
modified theorem Cardinal.power_zero