subsingleton_iff — Mathlib

English

For a LocalizationMap f, Subsingleton N is equivalent to 0 ∈ S.

Русский

Для отображения локализации f равенство «Subsingleton N» эквивалентно 0 ∈ S.

LaTeX

$$$\\text{Subsingleton}(N) \\iff 0 \\in S$$$

Lean4

theorem subsingleton_iff (f : LocalizationMap S N) : Subsingleton N ↔ 0 ∈ S :=
  ⟨fun _ ↦
    have ⟨c, eq⟩ := f.exists_of_eq 0 1 (Subsingleton.elim ..)
    by rw [mul_zero, mul_one] at eq; exact eq ▸ c.2,
    f.subsingleton⟩

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