coe_mapEquiv

Mathlib.Algebra.Group.Units.Equiv

URI: https://scilib.ai/kg/mathlib#Units.coe_mapEquiv

English

For x ∈ Mˣ, the image under mapEquiv h has underlying value equal to h(x), i.e., the unit image corresponds to h applied to x.

Русский

Для x ∈ Mˣ образ через mapEquiv h имеет основанное значение, равное h(x).

LaTeX

$$$(\\mathrm{mapEquiv}(h)\\, x) = h(x)\\quad \\text{in units}$$$

Lean4

@[simp]
theorem coe_mapEquiv (h : M ≃* N) (x : Mˣ) : (mapEquiv h x : N) = h x :=
  rfl

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

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

Разделы

Аффилиация

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