From b573906d089c4554e2ae8e2faf0161263aecc497 Mon Sep 17 00:00:00 2001 From: Artie Khovanov Date: Wed, 1 Jan 2025 13:43:09 +0000 Subject: [PATCH] yael comment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Algebra/Lie/Submodule.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean index b1865e620f82f..5c8bb02b5405d 100644 --- 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,