Theorem LinearMap.finite_iff_of_bijective

Modification history

2025-02-25 14:06
Mathlib/RingTheory/Finiteness/Basic.lean
feat(RingTheory): Artinian rings over Jacobson rings (#21904)
Added LinearMap.finite_iff_of_bijectiveView on Github →