Theorems · Theorem · number theory

NumberField.mixedEmbedding.negAt_preimage

∀ {K : Type u_1} [inst : Field K] (s : Set { w // w.IsReal }) (A : Set (NumberField.mixedEmbedding.mixedSpace K)),
  ⇑(NumberField.mixedEmbedding.negAt s) ⁻¹' A = ⇑(NumberField.mixedEmbedding.negAt s) '' A

negAt s A is also equal to the preimage of A by negAt s. This fact is used to simplify some proofs.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

1 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field