span_singleton_ne_top — Mathlib

English

If x is not a unit in a commutative semiring, then span({x}) ≠ top.

Русский

Если x не единица в коммутативном полупring, то span({x}) ≠ top.

LaTeX

$$$\\neg\\operatorname{IsUnit}(x) \\Rightarrow \\operatorname{span}(\\{x\\}) \\neq \\top$$$

Lean4

theorem span_singleton_ne_top {α : Type*} [CommSemiring α] {x : α} (hx : ¬IsUnit x) : Ideal.span ({ x } : Set α) ≠ ⊤ :=
  (Ideal.ne_top_iff_one _).mpr fun h1 =>
    let ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
    hx ⟨⟨x, y, mul_comm y x ▸ hy, hy⟩, rfl⟩

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