Theorems · Theorem · linear algebra

LinearMap.comp_eq_id_comm

∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] [IsStablyFiniteRing R] {f g : M →ₗ[R] M}, f ∘ₗ g = LinearMap.id ↔ g ∘ₗ f = LinearMap.id

In a finite-rank free module over a stably finite semiring, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

Defined in

Mathlib.LinearAlgebra.FiniteDimensional.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleModule.FreeModule.FiniteIsStablyFiniteRing