instNoZeroSMulDivisorsLocalizationAlgebraMapSubmonoidPrimeCompl_2

English

IsLocalization provides the universal localization of algebraic maps with respect to non-zero divisors.

Русский

IsLocalization задает универсальную локализацию алгебраических отображений по отношению к ненулевым делителям.

LaTeX

$$$\text IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L$$$

Lean4

instance [NoZeroSMulDivisors S T] : NoZeroSMulDivisors Sₚ Tₚ :=
  NoZeroSMulDivisors_of_isLocalization S T Sₚ Tₚ <|
    algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ <| Ideal.primeCompl_le_nonZeroDivisors P

Похожие утверждения