neg_apply'

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.neg_apply'

English

For ψ and a, (-ψ)(a) = (ψ(a))^{-1}.

Русский

Для ψ и a: (-ψ)(a) = (ψ(a))^{-1}.

LaTeX

$$$\forall a\in A,\ (-\psi)(a) = (\psi(a))^{-1}.$$$

Lean4

theorem neg_apply' (ψ : AddChar A M) (a : A) : (-ψ) a = (ψ a)⁻¹ :=
  map_neg_eq_inv _ _

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

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

Разделы

Аффилиация

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