Skip to content

Commit d4a3ea0

Browse files
committed
chore: fix implicit-reducible diamond in Lie subalgebras (#38260)
The following example fails on master, is fine on the branch: ``` example (I : LieIdeal R L) : ((LieIdeal.lieRing R L I).toBracket : Bracket ↥I ↥I) = (LieIdeal.lieRingModule (↥I) I).toBracket := by with_reducible_and_instances rfl ``` Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
1 parent b51f26d commit d4a3ea0

1 file changed

Lines changed: 6 additions & 0 deletions

File tree

Mathlib/Algebra/Lie/Ideal.lean

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,12 @@ theorem LieIdeal.toLieSubalgebra_toSubmodule (I : LieIdeal R L) :
7272
((I : LieSubalgebra R L) : Submodule R L) = LieSubmodule.toSubmodule I :=
7373
rfl
7474

75+
instance LieIdeal.bracket {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L]
76+
(I : LieIdeal R L) [Bracket L M] : Bracket I M where
77+
bracket x m := ⁅(x : L), m⁆
78+
79+
instance (I : LieIdeal R L) : Bracket I I := inferInstance
80+
7581
/-- An ideal of `L` is a Lie subalgebra of `L`, so it is a Lie ring. -/
7682
instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I :=
7783
inferInstanceAs <| LieRing I.toLieSubalgebra

0 commit comments

Comments
 (0)