From 6c6b8f987a25fc8097c95723b8c0b486d4520c6a Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sun, 19 Jul 2026 11:55:19 -0400 Subject: [PATCH 1/2] add theorem --- Mathlib/Algebra/FreeMonoid/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean index 806fe80a9bcdac..29b8ee72696733 100644 --- a/Mathlib/Algebra/FreeMonoid/Basic.lean +++ b/Mathlib/Algebra/FreeMonoid/Basic.lean @@ -172,6 +172,10 @@ theorem length_eq_zero : length a = 0 ↔ a = 1 := List.length_eq_zero_iff @[to_additive (attr := simp)] theorem length_of (m : α) : length (of m) = 1 := rfl +@[to_additive] +theorem length_surjective [hα : Nonempty α] : (@length α).Surjective := + hα.elim fun a n => ⟨FreeMonoid.ofList (List.replicate n a), by simp [length]⟩ + @[to_additive FreeAddMonoid.length_eq_one] theorem length_eq_one : length a = 1 ↔ ∃ m, a = FreeMonoid.of m := List.length_eq_one_iff From 82ccc48319a1e1aa95399849de54ff180d0aba75 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Wed, 22 Jul 2026 12:26:59 -0400 Subject: [PATCH 2/2] unname typeclass variable --- Mathlib/Algebra/FreeMonoid/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean index 29b8ee72696733..bc1c911462ccfa 100644 --- a/Mathlib/Algebra/FreeMonoid/Basic.lean +++ b/Mathlib/Algebra/FreeMonoid/Basic.lean @@ -173,8 +173,8 @@ theorem length_eq_zero : length a = 0 ↔ a = 1 := List.length_eq_zero_iff theorem length_of (m : α) : length (of m) = 1 := rfl @[to_additive] -theorem length_surjective [hα : Nonempty α] : (@length α).Surjective := - hα.elim fun a n => ⟨FreeMonoid.ofList (List.replicate n a), by simp [length]⟩ +theorem length_surjective [Nonempty α] : (@length α).Surjective := + ‹Nonempty α›.elim fun a n => ⟨FreeMonoid.ofList (List.replicate n a), by simp [length]⟩ @[to_additive FreeAddMonoid.length_eq_one] theorem length_eq_one : length a = 1 ↔ ∃ m, a = FreeMonoid.of m :=