inv_mk

Mathlib.Algebra.Notation.Prod

URI: https://scilib.ai/kg/mathlib#Prod.inv_mk

English

For any G, H with inverses, (a, b)^{-1} = (a^{-1}, b^{-1}).

Русский

Для любых G, H с обратимыми элементами, (a, b)^{-1} = (a^{-1}, b^{-1}).

LaTeX

$$(a,b)^{-1} = (a^{-1}, b^{-1})$$

Lean4

@[to_additive (attr := simp)]
theorem inv_mk (a : G) (b : H) : (a, b)⁻¹ = (a⁻¹, b⁻¹) :=
  rfl

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

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

Разделы

Аффилиация

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