Commit 2024-03-30 13:25 a77f5537
View on Github →feat(Algebra/Free): add length_pos lemma for free magmas (#11783)
This adds a length_pos lemma for multiplicative and additive free magmas.
Indeed, it sometimes happens in proofs that we need to know that the length of any element is indeed strictly positive.