inv_apply'

Mathlib.Algebra.Group.AddChar

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

English

For additive character ψ and a ∈ A, ψ^{-1}(a) = (ψ(a))^{-1}.

Русский

Для аддитивного характера ψ и a ∈ A верно ψ^{-1}(a) = (ψ(a))^{-1}.

LaTeX

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

Lean4

theorem inv_apply' (ψ : AddChar A M) (a : A) : ψ⁻¹ a = (ψ a)⁻¹ := by rw [inv_apply, map_neg_eq_inv]

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

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

Разделы

Аффилиация

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