Skip to content

feat(Algebra/FreeMonoid): FreeMonoid.length is surjective#41928

Open
plp127 wants to merge 1 commit into
leanprover-community:masterfrom
plp127:aliu/monoid-length
Open

feat(Algebra/FreeMonoid): FreeMonoid.length is surjective#41928
plp127 wants to merge 1 commit into
leanprover-community:masterfrom
plp127:aliu/monoid-length

add theorem

6c6b8f9
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jul 19, 2026 in 1m 26s