map_neg_eq_inv

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.map_neg_eq_inv

← MathLib Explorer

English

As in 7983, the values φ(a) are units for all a.

Русский

Как и в 7983, значения φ(a) являются единицами для всех a.

LaTeX

$$$\forall a\in A,\ IsUnit(φ(a)).$$$

Lean4

/-- An additive character maps negatives to inverses (when defined) -/
theorem map_neg_eq_inv (ψ : AddChar A M) (a : A) : ψ (-a) = (ψ a)⁻¹ :=
  by
  apply eq_inv_of_mul_eq_one_left
  simp only [← map_add_eq_mul, neg_add_cancel, map_zero_eq_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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