congr_symm — Mathlib

English

The inverse of the congruence between M ≃ₗ[R] P and N ≃ₗ[R] Q equals the congruence built from f.symm and g.symm: (congr f g).symm = congr f.symm g.symm.

Русский

Обратное сопоставление между M ≃ₗ[R] P и N ≃ₗ[R] Q эквивалентно конструированному из f.symm и g.symm сопоставлению: (congr f g).symm = congr f.symm g.symm.

LaTeX

$$$ (congr\\ f\\ g)^{-1} = congr\\ f^{-1}\\ g^{-1} $$$

Lean4

theorem congr_symm (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (congr f g).symm = congr f.symm g.symm :=
  rfl

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