feat(Algebra/Ring/BooleanRing): definitional lemmas for Bool ring operations (leanprover-community#38548)

Mathlib defines a ring structure on `Bool` but is missing definitional lemmas for the arithmetic operations.

Author: adomasbaliuka

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -541,3 +541,15 @@ instance : BooleanRing Bool where
   mul_zero a := by cases a <;> rfl
   nsmul := nsmulRec
   zsmul := zsmulRec
+
+theorem Bool.zero_eq_false : 0 = false := rfl
+
+theorem Bool.one_eq_true : 1 = true := rfl
+
+theorem Bool.add_eq_xor (b c : Bool) : b + c = (b ^^ c) := rfl
+
+theorem Bool.neg_eq_id (b : Bool) : -b = b := rfl
+
+theorem Bool.sub_eq_xor (b c : Bool) : b - c = (b ^^ c) := rfl
+
+theorem Bool.mul_eq_and (b c : Bool) : b * c = (b && c) := rfl