Commit 2026-07-27 16:25 d732046e

View on Github →

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

Estimated changes

Modified Mathlib/RingTheory/Finiteness/Basic.lean

modified theorem LinearMap.finite_iff_of_bijective