mem_zero_iff — Mathlib

English

An element x is in the zero fractional ideal iff x equals 0.

Русский

Элемент x принадлежит нулевому дробному идеалу тогда и только тогда, когда x = 0.

LaTeX

$$x ∈ (0 : FractionalIdeal S P) ↔ x = 0$$

Lean4

@[simp]
theorem mem_zero_iff {x : P} : x ∈ (0 : FractionalIdeal S P) ↔ x = 0 :=
  ⟨fun ⟨x', x'_mem_zero, x'_eq_x⟩ => by
    have x'_eq_zero : x' = 0 := x'_mem_zero
    simp [x'_eq_x.symm, x'_eq_zero], fun hx => ⟨0, rfl, by simp [hx]⟩⟩

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