span_natAbs — Mathlib

English

The principal ideal generated by a equals the principal ideal generated by |a| in ℤ.

Русский

Идеал, порожденный a, совпадает с идеалом, порожденным |a|, в целых.

LaTeX

$$$\\operatorname{Ideal.span} \\{ |a| \\} = \\operatorname{Ideal.span} \\{ a \\}.$$$

Lean4

theorem span_natAbs (a : ℤ) : Ideal.span ({(a.natAbs : ℤ)} : Set ℤ) = Ideal.span { a } :=
  by
  rw [Ideal.span_singleton_eq_span_singleton]
  exact (associated_natAbs _).symm

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