mem_idealLattice — Mathlib

English

Membership in the ideal lattice corresponds to the image under mixedEmbedding of the fractional ideal.

Русский

Принадлежность к идеальной решётке соответствует образу дробного идеала через смешанное вложение.

LaTeX

$$$ x \in mixedEmbedding.idealLattice K I \Leftrightarrow \exists y \; y \in I.1 \land mixedEmbedding K y = x $$$

Lean4

theorem mem_idealLattice {x : mixedSpace K} : x ∈ idealLattice K I ↔ ∃ y, y ∈ (I : Set K) ∧ mixedEmbedding K y = x := by
  simp [idealLattice]

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