instMulActionAlgEquiv — Mathlib

English

Applying the smul to an argument x yields the same as applying φ to σ^{-1}(x) after mk.

Русский

Применение дествия к аргументу x эквивалентно применению φ к σ^{-1}(x) после mk.

LaTeX

$$$ (\sigma \cdot \mathrm{mk}(\phi)) (x) = \mathrm{mk}(\phi)(\sigma^{-1}(x)) $$$

Lean4

/-- The action of the Galois group on infinite places. -/
@[simps! smul_coe_apply]
instance : MulAction (K ≃ₐ[k] K) (InfinitePlace K)
    where
  smul := fun σ w ↦ w.comap σ.symm
  one_smul := fun _ ↦ rfl
  mul_smul := fun _ _ _ ↦ rfl

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