negAt_apply_norm_isReal

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.negAt_apply_norm_isReal

English

The inverse of toMixed is volume-preserving.

Русский

Обратное отображение toMixed сохраняет объём.

LaTeX

$$volumePreserving_toMixed_symm : MeasurePreserving (toMixed K).symm$$

Lean4

theorem negAt_apply_norm_isReal (x : mixedSpace K) (w : { w // IsReal w }) : ‖(negAt s x).1 w‖ = ‖x.1 w‖ := by
  by_cases hw : w ∈ s <;> simp [hw]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru