fix

leanprover-community · Oct 28, 2024 · e3b75b0 · e3b75b0
1 parent 8333def
commit e3b75b0
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean
@@ -126,12 +126,14 @@ namespace LinearDisjoint
 variable (A B)
 
 /-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/
-theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B :=
-  Submodule.LinearDisjoint.one_left _
+theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B := by
+  rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
+  exact Submodule.LinearDisjoint.one_left _
 
 /-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/
-theorem bot_right : A.LinearDisjoint ⊥ :=
-  Submodule.LinearDisjoint.one_right _
+theorem bot_right : A.LinearDisjoint ⊥ := by
+  rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
+  exact Submodule.LinearDisjoint.one_right _
 
 end LinearDisjoint