smul_apply

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.smul_apply

English

The orbit-relation equivalence applied to the mk'' of w matches the restriction of w to k.

Русский

Применение эквивалентности орбит к mk'' бесконечного места совпадает с ограничением w на k.

LaTeX

$$$ \text{orbitRelEquiv}(\mathrm{Quotient.mk''}(w)) = \mathrm{comap}(w)(\mathrm{algebraMap}_{kK}) $$$

Lean4

@[simp]
theorem smul_apply (x) : (σ • w) x = w (σ.symm x) :=
  rfl

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

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

Разделы

Аффилиация

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