Theorems · Definition · commutative algebra

CharacterModule.congr

{R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] → [inst_4 : Module R B] → (A ≃ₗ[R] B) → CharacterModule A ≃ₗ[R] CharacterModule B

Two isomorphic modules have isomorphic character modules.

Defined in

Mathlib.Algebra.Module.CharacterModule

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupAddCommGroupModuleModule