Documentation
LeanPool
.
VirasoroProject
.
ToMathlib
.
Algebra
.
Lie
.
Abelian
Search
return to top
source
Imports
Init
Mathlib.Algebra.Lie.Abelian
Imported by
CommRing
.
isLieAbelian
LeanPool.VirasoroProject.ToMathlib.Algebra.Lie.Abelian
#
source
instance
CommRing
.
isLieAbelian
(
R
:
Type
u_1)
[
CommRing
R
]
:
IsLieAbelian
R