smul_eq_comap — Mathlib

English

There is an equivalence between the orbit of an infinite place under the Galois group and the infinite places of the base field.

Русский

Существует эквивалентность между орбитой бесконечного места и бесконечными местами базового поля.

LaTeX

$$$ \text{orbitRelEquiv} : \operatorname{Quotient}(\operatorname{MulAction}.\operatorname{orbitRel}(\operatorname{AlgEquiv}(k,K), \mathrm{InfinitePlace}(K))) \simeq \mathrm{InfinitePlace}(k) $$$

Lean4

theorem smul_eq_comap : σ • w = w.comap σ.symm :=
  rfl

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