Two-generator identities and unit-denominator transport

This neutral module extracts the reusable algebraic kernel formerly declared as Stafford38.LocalizationCorollaries.S38, Stafford38.LocalizationCorollaries.s38_of_rightClearing, and Stafford38.LocalizationCorollaries.s38_of_leftUnitClearing.

Source record: Stafford38 commit 1585e4c7, originally Stafford38/LocalizationCorollaries.lean and Stafford38/LeftDenominatorTransport.lean. The extracted declarations are application-independent; Stafford38-specific names and imports are intentionally absent. The written multiplication order is preserved.

def AlgebraicAnalysis.TwoGeneratorIdentity (R : Type u) [Ring R] : Prop

The two-generator identity in a ring, with the distinguished factor on the left of the first product and in the middle of the second.

Equations

• AlgebraicAnalysis.TwoGeneratorIdentity R = ∀ (d : R), d ≠ 0 → ∃ (F : R) (r : R) (s : R), 1 = d * r + F * d * s

theorem AlgebraicAnalysis.TwoGeneratorIdentity.of_rightUnitClearing {R : Type u} {L : Type v} [Ring R] [Ring L] {f : R →+* L} (hR : TwoGeneratorIdentity R) (hclear : ∀ (q : L), q ≠ 0 → ∃ (a : R) (s : R), IsUnit (f s) ∧ q * f s = f a) : TwoGeneratorIdentity L

Right-clearing transport of the two-generator identity.

theorem AlgebraicAnalysis.TwoGeneratorIdentity.of_leftUnitClearing {R : Type u} {L : Type v} [Ring R] [Ring L] {f : R →+* L} (hR : TwoGeneratorIdentity R) (hclear : ∀ (q : L), q ≠ 0 → ∃ (a : R) (u : L), IsUnit u ∧ u * q = f a) : TwoGeneratorIdentity L

Left-clearing transport of the two-generator identity.

theorem AlgebraicAnalysis.TwoGeneratorIdentity.of_rightOreLocalization {R : Type u} [Ring R] {S : Submonoid R} [OreLocalization.OreSet (OreRightLocalization.oppositeSubmonoid S)] (hR : TwoGeneratorIdentity R) : TwoGeneratorIdentity (OreRightLocalization.RightOreLocalization R S)

The two-generator identity is preserved by the right Ore localization implemented through the opposite ring.