Primitive elements of a set with respect to divisibility

An element n is primitive in a set S ⊆ ℕ if n ∈ S and no proper divisor of n is in S.

This concept appears naturally when studying sequences closed under "divisor inheritance" - if every member n of a sequence has the property that m * n is also in the sequence for coprime m, then the primitive elements generate the entire sequence.

Main definitions

• Set.IsPrimitive: A natural number n is primitive in S if n ∈ S and n.properDivisors is disjoint from S.
• Set.primitives: The set of primitive elements of S.

Main results

• Set.IsPrimitive.mem: A primitive element is in the set.
• Set.IsPrimitive.not_mem_of_properDivisor: Proper divisors of a primitive element are not in the set.
• Set.one_isPrimitive_iff: 1 is primitive in S iff 1 ∈ S.
• Set.prime_isPrimitive_iff: A prime p is primitive in S iff p ∈ S and 1 ∉ S.

def Set.IsPrimitive (S : Set ℕ) (n : ℕ) : Prop

An element n is primitive in a set S ⊆ ℕ if n ∈ S and no proper divisor of n is in S.

Equations

• S.IsPrimitive n = (n ∈ S ∧ Disjoint (↑n.properDivisors) S)

def Set.primitives (S : Set ℕ) : Set ℕ

The set of primitive elements of S.

Equations

• S.primitives = {n : ℕ | S.IsPrimitive n}

theorem Set.IsPrimitive.mem {S : Set ℕ} {n : ℕ} (h : S.IsPrimitive n) : n ∈ S

theorem Set.IsPrimitive.disjoint_properDivisors {S : Set ℕ} {n : ℕ} (h : S.IsPrimitive n) : Disjoint (↑n.properDivisors) S

theorem Set.IsPrimitive.not_mem_of_properDivisor {S : Set ℕ} {n d : ℕ} (h : S.IsPrimitive n) (hd : d ∈ n.properDivisors) : d ∉ S

theorem Set.IsPrimitive.not_mem_of_dvd_of_lt {S : Set ℕ} {n d : ℕ} (h : S.IsPrimitive n) (hdvd : d ∣ n) (hlt : d < n) : d ∉ S

theorem Set.isPrimitive_iff {S : Set ℕ} {n : ℕ} : S.IsPrimitive n ↔ n ∈ S ∧ ∀ d ∈ n.properDivisors, d ∉ S

theorem Set.isPrimitive_iff' {S : Set ℕ} {n : ℕ} (_hn : 0 < n) : S.IsPrimitive n ↔ n ∈ S ∧ ∀ (d : ℕ), d ∣ n → d < n → d ∉ S

theorem Set.mem_primitives_iff {S : Set ℕ} {n : ℕ} : n ∈ S.primitives ↔ S.IsPrimitive n

@[simp]

theorem Set.primitives_subset {S : Set ℕ} : S.primitives ⊆ S

theorem Set.one_isPrimitive_iff {S : Set ℕ} : S.IsPrimitive 1 ↔ 1 ∈ S

theorem Set.prime_isPrimitive_iff {S : Set ℕ} {p : ℕ} (hp : Nat.Prime p) : S.IsPrimitive p ↔ p ∈ S ∧ 1 ∉ S