Principal ideals of a subsemiring

For a subsemiring s of a commutative semiring A (for instance a subring or a subalgebra) and an element a ∈ s, the principal ideal a s of s consists of the elements of s that are a times an element of s. Read inside A, its n-th power is cut out of s by the scaled copy aⁿ • s.

Main results

• SubsemiringClass.mem_span_singleton_iff: x ∈ a s exactly when x = a * y for some y ∈ s.
• SubsemiringClass.coe_span_singleton_pow: (a s)ⁿ is the preimage in s of aⁿ • s ⊆ A.
• SubsemiringClass.coe_mem_smul_iff_dvd: for c, y ∈ s, y ∈ c • s exactly when c ∣ y in s.

theorem SubsemiringClass.mem_span_singleton_iff {A : Type u_1} {S : Type u_2} [CommSemiring A] [SetLike S A] [SubsemiringClass S A] (s : S) {a : A} (ha : a ∈ s) {x : ↥s} : x ∈ Ideal.span {⟨a, ha⟩} ↔ ∃ y ∈ s, a * y = ↑x

Membership in the principal ideal a s of a subsemiring s ∋ a: an element of s lies in it exactly when it is a times an element of s.

theorem SubsemiringClass.coe_span_singleton_pow {A : Type u_1} {S : Type u_2} [CommSemiring A] [SetLike S A] [SubsemiringClass S A] (s : S) {a : A} (ha : a ∈ s) (n : ℕ) : ↑(Ideal.span {⟨a, ha⟩} ^ n) = Subtype.val ⁻¹' (a ^ n • ↑s)

The n-th power of the principal ideal a s of a subsemiring s ∋ a is cut out of s by the scaled copy aⁿ • s.

theorem SubsemiringClass.coe_mem_smul_iff_dvd {A : Type u_1} {S : Type u_2} [CommSemiring A] [SetLike S A] [SubsemiringClass S A] (s : S) {c y : ↥s} : ↑y ∈ ↑c • ↑s ↔ c ∣ y

Membership of an element of a subsemiring s in the scaled copy c • s, for c ∈ s, is divisibility by c in s.