restrictRootsOfUnity_symm — Mathlib

English

Restricting a multiplicative equivalence and then taking the inverse is the same as taking the inverse and then restricting.

Русский

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

LaTeX

$$$(\restrictRootsOfUnity\ k).\text{symm} = \sigma^{\mathrm{symm}}_{k}$$$

Lean4

@[simp]
theorem restrictRootsOfUnity_symm (σ : R ≃* S) : (σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k :=
  rfl

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