instNoZeroSMulDivisorsLocalizationAlgebraMapSubmonoidPrimeCompl_1

English

Localization at a prime complement inherits NoZeroDivisors in the base structure, under faithful scalar action.

Русский

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

LaTeX

$$$\text{NoZeroDivisors} \; (R_p) \Rightarrow \text{NoZeroDivisors} \; (S_p)$$$

Lean4

instance : NoZeroSMulDivisors R Sₚ :=
  by
  have := IsLocalization.AtPrime.faithfulSMul Rₚ R P
  exact NoZeroSMulDivisors.trans_faithfulSMul R Rₚ _

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