absNorm_span_insert — Mathlib

English

The gcd of absNorm(span s) and the norm of an inserted element r divides absNorm(span(insert r s)).

Русский

Наибольший общий делитель absNorm(span s) и нормы r делит absNorm(span(insert r s)).

LaTeX

$$absNorm(span(insert r s)) ∣ gcd(absNorm(span s), (normℤ r).natAbs)$$

Lean4

@[simp]
theorem absNorm_span_insert (r : S) (s : Set S) :
    absNorm (span (insert r s)) ∣ gcd (absNorm (span s)) (Algebra.norm ℤ r).natAbs :=
  (dvd_gcd_iff _ _ _).mpr
    ⟨absNorm_dvd_absNorm_of_le (span_mono (Set.subset_insert _ _)),
      _root_.trans (absNorm_dvd_absNorm_of_le (span_mono (Set.singleton_subset_iff.mpr (Set.mem_insert _ _))))
        (by rw [absNorm_span_singleton])⟩

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