Theorems · Definition · linear algebra

LinearEquiv.ofEq

{R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p q : Submodule R M) → p = q → ↥p ≃ₗ[R] ↥q

Linear equivalence between two equal submodules.

Defined in

Mathlib.Algebra.Module.Submodule.Equiv

Cited by

32 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoid