Theorems · Definition · commutative algebra

addMonoidHomLequivInt

{A : Type u_9} →
  {B : Type u_10} →
    (R : Type u_11) →
      [inst : Semiring R] →
        [inst_1 : AddCommGroup A] → [inst_2 : AddCommGroup B] → [inst_3 : Module R B] → (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B

The R-linear equivalence between additive morphisms A →+ B and ℤ-linear morphisms A →ₗ[ℤ] B.

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

4 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommGroupAddCommGroupModule