elim_inv_inv — Mathlib

English

The inverse of a Sum.elim map is the Sum.elim of the inverses: Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹.

Русский

Обратное к Sum.elim равно Sum.elim от обращённых частей: Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹.

LaTeX

$$$ \mathrm{Sum.elim} a^{-1} b^{-1} = (\mathrm{Sum.elim} a b)^{-1} $$$

Lean4

@[to_additive]
theorem elim_inv_inv [Inv γ] : Sum.elim a⁻¹ b⁻¹ = (Sum.elim a b)⁻¹ :=
  (Sum.comp_elim Inv.inv a b).symm

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