feat(set_theory/cardinal): bit lemmas for exponentiation (#13010)

src/set_theory/cardinal.lean

@@ -375,6 +375,12 @@ instance : comm_semiring cardinal.{u} :=
   npow_zero'    := @power_zero,
   npow_succ'    := λ n c, by rw [nat.cast_succ, power_add, power_one, cardinal.mul_comm] }
 
+theorem power_bit0 (a b : cardinal) : a ^ (bit0 b) = a ^ b * a ^ b :=
+power_add
+
+theorem power_bit1 (a b : cardinal) : a ^ (bit1 b) = a ^ b * a ^ b * a :=
+by rw [bit1, ←power_bit0, power_add, power_one]
+
 @[simp] theorem one_power {a : cardinal} : 1 ^ a = 1 :=
 induction_on a $ assume α, (equiv.arrow_punit_equiv_punit α).cardinal_eq