Commit 2024-04-29 23:31 c1083208

View on Github →

feat(RingTheory/Finiteness): relax the condition of Module.Finite.exists_fin' (#12524) ... from CommSemiring R to Semiring R.

Estimated changes

modified theorem Module.Finite.exists_fin'