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
.
feat(RingTheory/Finiteness): relax the condition of Module.Finite.exists_fin'
(#12524)
... from CommSemiring R
to Semiring R
.