Documentation

LeanPool.SelbergSieve4.Tactic.AesopDiv

LeanPool.SelbergSieve4.Tactic.AesopDiv #

def Sieve.MyDvd (a b : ℕ) :

Wrapper predicate for divisibility used by the Divisibility Aesop rule set.

Equations

Sieve.MyDvd a b = (a ∣ b)

Instances For

@[simp]

theorem Sieve.myDvd_iff (a b : ℕ) :

Sieve.MyDvd a b ↔ a ∣ b

def Sieve.aesopDiv :

Lean.ParserDescr

Run aesop using the local divisibility rule set with simplification disabled.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Sieve.aesopDiv? :

Lean.ParserDescr

Run aesop? using the local divisibility rule set with simplification disabled.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Sieve.dvd_of_myDvd (a b : ℕ) :

Sieve.MyDvd a b → a ∣ b

theorem Sieve.myDvd_of_dvd (a b : ℕ) :

a ∣ b → Sieve.MyDvd a b

theorem Sieve.myDvd_trans {a b c : ℕ} :

Sieve.MyDvd a b → Sieve.MyDvd b c → Sieve.MyDvd a c

theorem Sieve.myDvd_of_mem_divisors {a b : ℕ} :

a ∈ b.divisors → Sieve.MyDvd a b

theorem Sieve.myDvd_of_mem_primeFactors {a b : ℕ} :

a ∈ b.primeFactors → Sieve.MyDvd a b

theorem Sieve.eq_zero_of_zero_myDvd (a : ℕ) :

Sieve.MyDvd 0 a → a = 0

theorem Sieve.zero_mem_divisors (a : ℕ) (h : 0 ∈ a.divisors) :

theorem Sieve.mem_zero_divisors (a : ℕ) (h : a ∈ Nat.divisors 0) :

theorem Sieve.zero_lt_zero (h : 0 < 0) :

theorem Sieve.test {n m : ℕ} :

n ∣ m ∧ m ≠ 0 → n ∈ m.divisors

theorem Sieve.dvd_of_gcd_dvd_left (a b c : ℕ) (h : Sieve.MyDvd c (a.gcd b)) :

Sieve.MyDvd c a

theorem Sieve.dvd_of_gcd_dvd_right (a b c : ℕ) (h : Sieve.MyDvd c (a.gcd b)) :

Sieve.MyDvd c b

theorem Sieve.gcd_dvd_of_dvd_left (a b c : ℕ) (h : Sieve.MyDvd a c) :

Sieve.MyDvd (a.gcd b) c

theorem Sieve.gcd_dvd_of_dvd_right (a b c : ℕ) (h : Sieve.MyDvd b c) :

Sieve.MyDvd (a.gcd b) c

theorem Sieve.gcd_myDvd_left (a b : ℕ) :

Sieve.MyDvd (a.gcd b) a

theorem Sieve.gcd_myDvd_right (a b : ℕ) :

Sieve.MyDvd (a.gcd b) b

theorem Sieve.gcd_eq_zero_left (a b : ℕ) (h : a.gcd b = 0) :

a = 0

theorem Sieve.gcd_eq_zero_right (a b : ℕ) (h : a.gcd b = 0) :

b = 0

theorem Sieve.dvd_of_lcm_dvd_left (a b c : ℕ) (h : Sieve.MyDvd (a.lcm b) c) :

Sieve.MyDvd a c

theorem Sieve.dvd_of_lcm_dvd_right (a b c : ℕ) (h : Sieve.MyDvd (a.lcm b) c) :

Sieve.MyDvd b c

theorem Sieve.dvd_lcm_of_dvd_left (a b c : ℕ) (h : Sieve.MyDvd c a) :

Sieve.MyDvd c (a.lcm b)

theorem Sieve.dvd_lcm_of_dvd_right (a b c : ℕ) (h : Sieve.MyDvd c b) :

Sieve.MyDvd c (a.lcm b)

theorem Sieve.myDvd_lcm_left (a b : ℕ) :

Sieve.MyDvd a (a.lcm b)

theorem Sieve.myDvd_lcm_right (a b : ℕ) :

Sieve.MyDvd b (a.lcm b)

theorem Sieve.lcm_eq_zero_left (a b : ℕ) (h : a.lcm b = 0) :

a = 0 ∨ b = 0

theorem Sieve.squarefree_of_myDvd (a b : ℕ) (hb : Squarefree b) (h : Sieve.MyDvd a b) :