Theorems · Theorem · linear algebra

Module.End.injective_of_surjective_fin

∀ {A : Type u_3} [inst : Semiring A] [IsStablyFiniteRing A] {n : ℕ} {f : Module.End A (Fin n → A)},
  Function.Surjective ⇑f → Function.Injective ⇑f

Module.End.injective_of_surjective is the more general version for finite free A-modules not necessarily of the form Fin n → A, but this version requires less imports.

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringIsStablyFiniteRing