Symm (#5)

* Symm * Delete comment
fpvandoorn · Apr 19, 2024 · c2c03dd · c2c03dd
1 parent 43732dd
commit c2c03dd
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean
@@ -34,7 +34,11 @@ namespace IsConjExponent
 
 lemma one_le_left (hpq : p.IsConjExponent q) : 1 ≤ p := sorry
 
-lemma symm (hpq : p.IsConjExponent q) : q.IsConjExponent p := sorry
+lemma symm (hpq : p.IsConjExponent q) : q.IsConjExponent p where
+  inv_add_inv_conj := by
+    rw [add_comm]
+    exact hpq.inv_add_inv_conj
+
 
 lemma one_le_right (hpq : p.IsConjExponent q) : 1 ≤ q := hpq.symm.one_le_left