α : Type u_1
β : Type ?u.38685
γ : Type ?u.38688
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ↑ofBoolAlg a + ↑ofBoolAlg b
α : Type u_1
β : Type ?u.38685
γ : Type ?u.38688
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg (a ∆ b) = ↑ofBoolAlg a + ↑ofBoolAlg b
rw [symmDiff_eq_sup_sdiff_inf]
no goals
α : Type u_1
β : Type ?u.38685
γ : Type ?u.38688
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ↑ofBoolAlg a + ↑ofBoolAlg b
exact of_boolalg_symm_diff_aux _ _