mk_ne_zero' — Mathlib

English

In a commutative semiring, the associator class of the principal ideal generated by r is nonzero iff r ≠ 0.

Русский

В коммутативном полузкольке класс ассоциированности порожденного идеала (r) не равен нулю тогда и только тогда, когда r ≠ 0.

LaTeX

$$$\\operatorname{Associates}.mk(\\operatorname{Ideal.span}\\{r\\}) \\neq 0 \\iff r \\neq 0$$$

Lean4

theorem mk_ne_zero' {R : Type*} [CommSemiring R] {r : R} : Associates.mk (Ideal.span { r } : Ideal R) ≠ 0 ↔ r ≠ 0 := by
  rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]

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