sec_snd_ne_zero — Mathlib

English

Same as above: for nontrivial R and M ⊆ nonZeroDivisors(R), every x ∈ S has nonzero numerator in its sec representation.

Русский

То же самое: для не тривиального R и M ⊆ nonZeroDivisors(R) любой x ∈ S имеет ненулый числитель в сек-представлении.

LaTeX

$$$[\\text{Nontrivial } R]\\ (hM : M \\leq nonZeroDivisors\\ R)\\ \\forall x:\\, S,\\ IsLocalization.sec M x).\\snd.\\val \\neq 0$$$

Lean4

theorem sec_snd_ne_zero [Nontrivial R] (hM : M ≤ nonZeroDivisors R) (x : S) : ((sec M x).snd : R) ≠ 0 :=
  nonZeroDivisors.coe_ne_zero ⟨(sec M x).snd.val, hM (sec M x).snd.property⟩

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