Si m divide a n o a k, entonces m divide a nk
Demostrar con Lean4 que si m divide a n o a k, entonces m divide a nk.
Para ello, completar la siguiente teoría de Lean4:
Demostrar con Lean4 que si m divide a n o a k, entonces m divide a nk.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable {m n k : ℕ} example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by sorry |