s

ErikEk · ErikEk · commit f17e657f0416 · 2025-10-01T19:22:37.000+02:00
diff --git a/group_theory.lean b/group_theory.lean
@@ -0,0 +1,4 @@
+import Mathlib.Data.Real.Basic
+
+example {G : Type} [Group G] (g : G) : 1 * g = g := by
+  apply one_mul
