yael comment

Co-authored-by: Yaël Dillies <[email protected]>
leanprover-community · Jan 1, 2025 · b573906 · b573906
1 parent 1af97e7
commit b573906
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean
@@ -542,6 +542,7 @@ theorem iSup_induction' {ι} (N : ι → LieSubmodule R L M) {C : (x : M) → (x
   · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
     exact ⟨_, hadd _ _ _ _ Cx Cy⟩
 
+-- TODO(Yaël): turn around
 theorem disjoint_iff_toSubmodule :
     Disjoint N N' ↔ Disjoint (N : Submodule R M) (N' : Submodule R M) := by
   rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,