principalUnitGroupEquiv_apply — Mathlib

English

For a in A.principalUnitGroup, its image under the principalUnitGroupEquiv, regarded as an element of K^×, coincides with a.

Русский

Для элемента a ∈ A.principalUnitGroup образ a под эквивалентом principalUnitGroupEquiv, рассмотренный как элемент K^×, совпадает с a.

LaTeX

$$$(\mathrm{principalUnitGroupEquiv}(A)\, a : A^{\times}) : K^× = (a : K^×)$$$

Lean4

theorem principalUnitGroupEquiv_apply (a : A.principalUnitGroup) :
    (((principalUnitGroupEquiv A a : Aˣ) : A) : K) = (a : Kˣ) :=
  rfl

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