nonempty_oreSet_of_strongRankCondition

English

If R satisfies StrongRankCondition, then the OreSet of nonZeroDivisors is nonempty.

Русский

Если R удовлетворяет StrongRankCondition, то OreSet не нулевых делителей непуст.

LaTeX

$$Nonempty(\operatorname{OreLocalization.OreSet} (\operatorname{nonZeroDivisors} R))$$

Lean4

theorem nonempty_oreSet_of_strongRankCondition [StrongRankCondition R] : Nonempty (OreLocalization.OreSet R⁰) :=
  by
  by_contra! h
  have := aleph0_le_rank_of_isEmpty_oreSet h
  rw [rank_self] at this
  exact this.not_gt one_lt_aleph0

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