ofUnitHom_eq

Mathlib.NumberTheory.MulChar.Basic

URI: https://scilib.ai/kg/mathlib#MulChar.ofUnitHom_eq

English

For χ and a ∈ Units R, the coercion of the equivalence image equals χ a.

Русский

Для χ и a ∈ Units R, схождение изображения эквивалентности равно χ a.

LaTeX

$$$↑(\text{equivToUnitHom } χ\, a) = χ(a).$$$

Lean4

@[simp]
theorem ofUnitHom_eq (χ : Rˣ →* R'ˣ) : ofUnitHom χ = equivToUnitHom.symm χ :=
  rfl

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

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

Разделы

Аффилиация

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