mem_one_iff — Mathlib

English

An element x of P lies in the unit fractional ideal 1 if and only if x is the image of some r ∈ R under algebraMap.

Русский

Элемент x из P принадлежит единичному дробному идеалу 1 тогда и только тогда, когда x является образцом какого-либо r из R под алгебраическим отображением.

LaTeX

$$$x \in (1 : \mathrm{FractionalIdeal} S P) \iff \exists r : R, \ algebraMap R P(r) = x$$$

Lean4

theorem mem_one_iff {x : P} : x ∈ (1 : FractionalIdeal S P) ↔ ∃ x' : R, algebraMap R P x' = x :=
  Iff.intro (fun ⟨x', _, h⟩ => ⟨x', h⟩) fun ⟨x', h⟩ => ⟨x', ⟨⟩, h⟩

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