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 |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ (∀ k, m, n ∈ ℕ)[k ∣ \gcd(m, n) ↔ k ∣ m ∧ k ∣ n] \]
Por el lema,
\[ 3 ∣ \gcd(6, 15) \]
se reduce a
\[ 3 ∣ 6 ∧ 3 ∣ 15 \]
que se verifican fácilmente.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 |
import Mathlib.Data.Real.Basic import Mathlib.Data.Nat.GCD.Basic open Nat -- 1ª demostración -- =============== example : 3 ∣ gcd 6 15 := by rw [dvd_gcd_iff] -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15 constructor . -- 3 ∣ 6 norm_num . -- ⊢ 3 ∣ 15 norm_num -- 2ª demostración -- =============== example : 3 ∣ gcd 6 15 := by rw [dvd_gcd_iff] -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15 constructor <;> norm_num -- Lemas usados -- ============ -- variable (k m n : ℕ) -- #check (dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
