lean_workbook_plus_55081
ProvedIf and then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55081 (a b c d m : ℤ) (h₁ : a ≡ b [ZMOD m]) (h₂ : c ≡ d [ZMOD m]) : a * c ≡ b * d [ZMOD m] := by sorry
Source
If and then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_55081 (a b c d m : ℤ) (h₁ : a ≡ b [ZMOD m]) (h₂ : c ≡ d [ZMOD m]) : a * c ≡ b * d [ZMOD m] := by sorry