to_map_ne_zero_of_mem_nonZeroDivisors

English

If R is nontrivial and M ⊆ nonZeroDivisors(R), then for every x ∈ S, the denominator component of the sec representation of x is nonzero in R.

Русский

Пусть R не тривиально и M ⊆ nonZeroDivisors(R). Тогда для каждого x ∈ S знаменатель сек представления x не нулевой в R.

LaTeX

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

Lean4

protected theorem to_map_ne_zero_of_mem_nonZeroDivisors [Nontrivial R] (hM : M ≤ nonZeroDivisors R) {x : R}
    (hx : x ∈ nonZeroDivisors R) : algebraMap R S x ≠ 0 :=
  by
  rw [Ne, to_map_eq_zero_iff S hM]
  exact nonZeroDivisors.ne_zero hx

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