map_inv

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.GeneralLinearGroup.map_inv

English

The map preserves inverses: map f (g^{-1}) = (map f g)^{-1}.

Русский

Отображение сохраняет обратные: map f (g^{-1}) = (map f g)^{-1}.

LaTeX

$$\\mathrm{map}\\,f\\ (g^{-1}) = (\\mathrm{map}\\,f\\,g)^{-1}$$

Lean4

protected theorem map_inv (g : GL n R) : map f g⁻¹ = (map f g)⁻¹ := by simp only [map_inv]

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

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

Разделы

Аффилиация

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