instInvolutiveInv — Mathlib

English

If M and N have involutive inverses, then the product M × N has an involutive inverse given componentwise, i.e., (a, b)^{-1} = (a^{-1}, b^{-1}), and applying inverse twice returns the original pair.

Русский

Если у M и N есть инволютивные обратные, то произведение M × N имеет обратное, заданное по компонентам: (a,b)^{-1} = (a^{-1}, b^{-1}), и дважды применённое обратное восстанавливает исходную пару.

LaTeX

$$$(a,b)^{-1} = (a^{-1}, b^{-1}) \quad \text{and} \quad ((a,b)^{-1})^{-1} = (a,b)$$$

Lean4

@[to_additive]
instance [InvolutiveInv M] [InvolutiveInv N] : InvolutiveInv (M × N) :=
  { inv_inv := fun _ => Prod.ext (inv_inv _) (inv_inv _) }

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