realMixedSpace — Mathlib

English

The inverse of the mixedSpaceToRealMixedSpace map preserves volume.

Русский

Обратная карта mixedSpaceToRealMixedSpace сохраняет объем.

LaTeX

$$$\\operatorname{vol} \\circ (\\mathrm{mixedSpaceToRealMixedSpace}(K))^{-1} = \\operatorname{vol}$$$

Lean4

/-- The real mixed space `ℝ^r₁ × (ℝ × ℝ)^r₂` with `(r₁, r₂)` the signature of `K`.
-/
abbrev realMixedSpace :=
  ({ w : InfinitePlace K // IsReal w } → ℝ) × ({ w : InfinitePlace K // IsComplex w } → ℝ × ℝ)

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