Localization interface for derivation-Ore extensions

The proposition below is the exact output expected from a theorem saying that localizing a derivation-Ore extension at coefficients gives the derivation-Ore extension of the localized coefficient ring. It packages data and its compatibility law; it does not assert that the data exist.

def AlgebraicAnalysis.OreLocalizationExtension.IsDerivationOreLocalization {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (S : Submonoid B) [OreLocalization.OreSet S] [OreLocalization.OreSet (Submonoid.map (↑(OreAssociativity.normalCoefficient D)) S)] : Prop

Existence of data identifying the localization of NormalOre D along coefficient denominators with a derivation-Ore extension of the localized coefficient ring. Ore-ness of both denominator sets remains an explicit hypothesis.

Equations

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