absNorm_span_singleton — Mathlib

English

The norm of the span of a single element r equals the ℤ-norm of r.

Русский

Норма пространства, порождаемого одним элементом r, равна норме ℤ от r.

LaTeX

$$absNorm(span({r})) = (normℤ r).natAbs$$

Lean4

@[simp]
theorem absNorm_span_singleton (r : S) : absNorm (span ({ r } : Set S)) = (Algebra.norm ℤ r).natAbs :=
  by
  rw [Algebra.norm_apply]
  by_cases hr : r = 0
  ·
    simp only [hr, Ideal.span_zero, Ideal.absNorm_bot, LinearMap.det_zero'', Set.singleton_zero, map_zero,
      Int.natAbs_zero]
  letI := Ideal.finiteQuotientOfFreeOfNeBot (span { r }) (mt span_singleton_eq_bot.mp hr)
  let b := Module.Free.chooseBasis ℤ S
  rw [← natAbs_det_equiv _ (b.equiv (basisSpanSingleton b hr) (Equiv.refl _))]
  congr
  refine b.ext fun i => ?_
  simp

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