lean_workbook_plus_55534
ProvedUsing logical equivalences, show that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55534 (p q : Prop) : p ∨ (p ∧ q) ↔ p := by sorry
Source
Using logical equivalences, show that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_55534 (p q : Prop) : p ∨ (p ∧ q) ↔ p := by sorry