liesOver_span_absNorm — Mathlib

English

For a ring R and an ideal I of R, the ideal I lies over the principal ideal generated by absNorm(under ℤ I) in the integers.

Русский

Для кольца R и идеала I ⊆ R идеал I лежит над главным идеалом, порожденным absNorm(under ℤ I) в целых.

LaTeX

$$$I \text{ lies over } \operatorname{span}\{ \operatorname{absNorm}(\operatorname{under} \mathbb{Z} I) \}$$$

Lean4

instance liesOver_span_absNorm (I : Ideal R) : I.LiesOver (span {(absNorm (under ℤ I) : ℤ)}) := by
  rw [liesOver_iff, under_def, Int.ideal_span_absNorm_eq_self]

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