lean_workbook_plus_62545
ProvedIf , then is ?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62545 (n m a b : ℤ) (h₁ : n > 0 ∧ m > 0) (hab : a ≡ b [ZMOD m]) : n * a ≡ n * b [ZMOD n * m] := by sorry
Source
If , then is ?
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_62545 (n m a b : ℤ) (h₁ : n > 0 ∧ m > 0) (hab : a ≡ b [ZMOD m]) : n * a ≡ n * b [ZMOD n * m] := by sorry