Theorems · Theorem · nonassociative algebras

LieAlgebra.Basis.ext

∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} {inst : Finite ι} {inst_1 : CommRing R} {inst_2 : LieRing L}
  {inst_3 : LieAlgebra R L} {H : LieSubalgebra R L} {x y : LieAlgebra.Basis ι H},
  x.A = y.A → x.h = y.h → x.e = y.e → x.f = y.f → x = y

Defined in

Mathlib.Algebra.Lie.Basis.Basic

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound