We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f10b6ee commit 725af7fCopy full SHA for 725af7f
lie_algebras.lean
@@ -4,7 +4,6 @@ import Mathlib.Tactic
4
variable (L M : Type) [LieRing L] [LieRing M]
5
example : ∀ (x y z : L), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆ := by
6
apply add_lie
7
-
8
example : ∀ (x : L), ⁅x, x⁆ = 0 := by
9
apply lie_self
10
example : ∀ (x y m : L), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ := by
0 commit comments