From a569bca94b3ce573e7cf2435526516ff97482798 Mon Sep 17 00:00:00 2001 From: gray311 Date: Wed, 16 Oct 2024 03:09:44 +0000 Subject: [PATCH] LeanAgent Proofs --- Coxeter/StrongExchange.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Coxeter/StrongExchange.lean b/Coxeter/StrongExchange.lean index 5fa5aac5..3ca1958c 100644 --- a/Coxeter/StrongExchange.lean +++ b/Coxeter/StrongExchange.lean @@ -115,7 +115,9 @@ local notation "S'" => CoxeterMatrix.SimpleRefl (toMatrix S) def invmap (S:Set G) [CoxeterSystem G S] : G →* CoxeterMatrix.toGroup (toMatrix S) := monoidLift.mapLift (CoxeterMatrix.of_relation (toMatrix S)) lemma invmap.of_eq {S:Set G} [CoxeterSystem G S] {s :S} : invmap S s = s := by - sorry + simp [CoxeterSystem.Presentation.invmap] + unfold CoxeterSystem.toMatrix + apply CoxeterSystem.monoidLift.mapLift.of def invmap_map_eq_id : MonoidHom.comp (invmap S) (map S) = MonoidHom.id G':= by ext x