Finite intersections in a right Ore domain

Right ideals are represented as left modules over the opposite ring. The right Ore condition is kept as an explicit common-right-multiple hypothesis; this module does not depend on a particular localization construction.

def AlgebraicAnalysis.OreRightIntersection.RightOreCondition (R : Type u_2) [SemigroupWithZero R] : Prop

Every pair of nonzero elements has a nonzero common right multiple.

Equations

• AlgebraicAnalysis.OreRightIntersection.RightOreCondition R = ∀ ⦃a b : R⦄, a ≠ 0 → b ≠ 0 → ∃ (x : R) (y : R), a * x = b * y ∧ a * x ≠ 0

theorem AlgebraicAnalysis.OreRightIntersection.exists_mem_finset_rightIdeals {R : Type u_1} [Ring R] [IsDomain R] {ι : Type u_2} (s : Finset ι) (I : ι → Submodule Rᵐᵒᵖ R) (hI : ∀ i ∈ s, ∃ x ∈ I i, x ≠ 0) (hOre : RightOreCondition R) : ∃ (x : R), x ≠ 0 ∧ ∀ i ∈ s, x ∈ I i

A finite family of nonzero right ideals has a nonzero common element.

The right ideals are left Rᵐᵒᵖ-submodules, so multiplying a member on the right is expressed by scalar multiplication by MulOpposite.op.