faithfulSMul — Mathlib

English

The natural action of R on Localization.AtPrime S P is faithful; i.e., if r ∈ R acts as zero on Localization.AtPrime S P, then r = 0.

Русский

Естественное действие R на Localization.AtPrime S P является верным (нефальшивым); если элемент r действует как ноль на локализации, то r = 0.

LaTeX

$$$$ \text{FaithfulSMul } R\ S $$$$

Lean4

theorem _root_.IsLocalization.AtPrime.faithfulSMul (R : Type*) [CommRing R] [NoZeroDivisors R] [Algebra R S]
    (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : FaithfulSMul R S :=
  by
  rw [faithfulSMul_iff_algebraMap_injective, IsLocalization.injective_iff_isRegular P.primeCompl]
  exact fun ⟨_, h⟩ ↦ isRegular_of_ne_zero <| by aesop

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