Theorem LinearMap.finite_iff_of_bijective

Modification history

2026-07-27 16:25

Mathlib/RingTheory/Finiteness/Basic.lean

refactor: generalize `Module.Finite.of_surjective` to arbitrary ring homomorphisms (#42054)

Modified LinearMap.finite_iff_of_bijective View on Github →

2025-02-25 14:06

Mathlib/RingTheory/Finiteness/Basic.lean

feat(RingTheory): Artinian rings over Jacobson rings (#21904)

Added LinearMap.finite_iff_of_bijective View on Github →