congr — Mathlib

English

Two isomorphic modules have isomorphic character modules. If e: A ≃ₗ[R] B is a linear equivalence, then CharacterModule A ≃ₗ[R] CharacterModule B.

Русский

Два изоморфных модуля имеют изоморфные характеристические модули. Если e: A ≃ₗ[R] B, то CharacterModule A ≃ₗ[R] CharacterModule B.

LaTeX

$$$\text{If } e: A \simeq B, \text{ then } \mathrm{CharacterModule}(A) \simeq \mathrm{CharacterModule}(B).$$$

Lean4

/-- Two isomorphic modules have isomorphic character modules.
-/
def congr (e : A ≃ₗ[R] B) : CharacterModule A ≃ₗ[R] CharacterModule B :=
  .ofLinear (dual e.symm) (dual e) (by ext c _; exact congr(c $(e.right_inv _)))
    (by ext c _; exact congr(c $(e.left_inv _)))

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