3 divide al máximo común divisor de 6 y 15
Demostrar con Lean4 que 3 divide al máximo común divisor de 6 y 15.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic import Mathlib.Data.Nat.GCD.Basic open Nat example : 3 ∣ gcd 6 15 := by sorry |