Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Patrick Stevens

! This file was ported from Lean 3 source module data.nat.choose.dvd
! leanprover-community/mathlib commit 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Prime

/-!
# Divisibility properties of binomial coefficients
-/


namespace Nat

open Nat

namespace Prime

variable {p a b k : 
ℕ: Type
ℕ
} theorem
dvd_choose_add: Prime p → a < p → b < p → p ≤ a + b → p ∣ choose (a + b) a
dvd_choose_add
(
hp: Prime p
hp
:
Prime: ℕ → Prop
Prime
p) (
hap: a < p
hap
: a < p) (
hbp: b < p
hbp
: b < p) (
h: p ≤ a + b
h
: p ≤ a + b) : p ∣
choose: ℕ → ℕ → ℕ
choose
(a + b) a :=

Goals accomplished! 🐙
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ choose (a + b) b * a ! * b !


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ choose (a + b) a * a ! * b !


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ choose (a + b) a * a ! ∨ p ∣ b !


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ∣ a !) ∨ p ∣ b !


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ∣ b !


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b


p ∣ choose (a + b) a
p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b


p ∣ choose (a + b) a

Goals accomplished! 🐙
#align nat.prime.dvd_choose_add
Nat.Prime.dvd_choose_add: ∀ {p a b : ℕ}, Prime p → a < p → b < p → p ≤ a + b → p ∣ choose (a + b) a
Nat.Prime.dvd_choose_add
lemma
dvd_choose: Prime p → a < p → b - a < p → p ≤ b → p ∣ choose b a
dvd_choose
(
hp: Prime p
hp
:
Prime: ℕ → Prop
Prime
p) (
ha: a < p
ha
: a < p) (
hab: b - a < p
hab
: b - a < p) (
h: p ≤ b
h
: p ≤ b) : p ∣
choose: ℕ → ℕ → ℕ
choose
b a := have : a + (b - a) = b :=
Nat.add_sub_of_le: ∀ {a b : ℕ}, a ≤ b → a + (b - a) = b
Nat.add_sub_of_le
(
ha: a < p
ha
.
le: ∀ {α : Type ?u.606} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le
.
trans: ∀ {α : Type ?u.662} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans
h: p ≤ b
h
)
this: a + (b - a) = b
this
▸
hp: Prime p
hp
.
dvd_choose_add: ∀ {p a b : ℕ}, Prime p → a < p → b < p → p ≤ a + b → p ∣ choose (a + b) a
dvd_choose_add
ha: a < p
ha
hab: b - a < p
hab
(
this: a + (b - a) = b
this
.
symm: ∀ {α : Sort ?u.697} {a b : α}, a = b → b = a
symm
▸
h: p ≤ b
h
) #align nat.prime.dvd_choose
Nat.Prime.dvd_choose: ∀ {p a b : ℕ}, Prime p → a < p → b - a < p → p ≤ b → p ∣ choose b a
Nat.Prime.dvd_choose
lemma
dvd_choose_self: ∀ {p k : ℕ}, Prime p → k ≠ 0 → k < p → p ∣ choose p k
dvd_choose_self
(
hp: Prime p
hp
:
Prime: ℕ → Prop
Prime
p) (
hk: k ≠ 0
hk
: k ≠
0: ?m.744
0
) (
hkp: k < p
hkp
: k < p) : p ∣
choose: ℕ → ℕ → ℕ
choose
p k :=
hp: Prime p
hp
.
dvd_choose: ∀ {p a b : ℕ}, Prime p → a < p → b - a < p → p ≤ b → p ∣ choose b a
dvd_choose
hkp: k < p
hkp
(
sub_lt: ∀ {n m : ℕ}, 0 < n → 0 < m → n - m < n
sub_lt
((
zero_le: ∀ (n : ℕ), 0 ≤ n
zero_le
_).
trans_lt: ∀ {α : Type ?u.810} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
trans_lt
hkp: k < p
hkp
)
hk: k ≠ 0
hk
.
bot_lt: ∀ {α : Type ?u.874} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≠ ⊥ → ⊥ < a
bot_lt
)
le_rfl: ∀ {α : Type ?u.938} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align nat.prime.dvd_choose_self
Nat.Prime.dvd_choose_self: ∀ {p k : ℕ}, Prime p → k ≠ 0 → k < p → p ∣ choose p k
Nat.Prime.dvd_choose_self
end Prime end Nat