unitary_eq — Mathlib

English

The unitary elements of the unit group Rˣ coincide with the comap of unitary elements of R via the coeHom map.

Русский

Единичные элементы группы единиц Rˣ совпадают с образами унитарных элементов R через отображение сопряжения.

LaTeX

$$$ \mathrm{unitary}(R^{\times}) = (\mathrm{unitary}(R)).\mathrm{comap}(\mathrm{Units.coeHom} R) $$$

Lean4

theorem _root_.Units.unitary_eq : unitary Rˣ = (unitary R).comap (Units.coeHom R) :=
  by
  ext
  simp [unitary.mem_iff, Units.ext_iff]

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