volume_preserving_negAt — Mathlib

English

The image of the ring of integers under the mixed embedding is a lattice in the mixed space.

Русский

Образ кольца целых под смешанным вложением образует решётку в смешанном пространстве.

LaTeX

$$ToMixed.image(\mathcal{O}_K) = Z\text{-lattice in mixedSpace(K)}$$

Lean4

/-- `negAt` preserves the volume . -/
theorem volume_preserving_negAt [NumberField K] : MeasurePreserving (negAt s) :=
  by
  refine MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)
  by_cases hw : w ∈ s
  · simp_rw [if_pos hw]
    exact Measure.measurePreserving_neg _
  · simp_rw [if_neg hw]
    exact MeasurePreserving.id _

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