Commit 2024-09-10 08:39 a5f50bc3

View on Github →

feat: generalize Module.Finite.finite_basis to semirings (#16655)

Estimated changes

Modified Mathlib/RingTheory/Finiteness.lean

modified theorem Module.Finite.finite_basis