# 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.