Mathlib Map

Theorems · Definition · nonassociative algebras

LieEquiv.refl

{R : Type u} → {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → L₁ ≃ₗ⁅R⁆ L₁

Lie algebra equivalences are reflexive.

Defined in
Mathlib.Algebra.Lie.Basic
Cited by
4 results in Mathlib
Foundations
Depth 31 from the axioms · uses propext, Quot.sound
Assumes
CommRingLieRingLieAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

LieAlgebra.Extension.ofAlg · cited by 1Extension.ofAlgLieEquiv.self_trans_symm · cited by 1LieEquiv.self_trans_symmLieEquiv.symm_trans_self · cited by 0LieEquiv.symm_trans_selfLieAlgebra.loopAlgebraEquivLaurent · cited by 0LieAlgebra.loopAlgebraEqu…LieEquiv.refl_apply · cited by 0LieEquiv.refl_applyLieEquiv.refl_symm · cited by 0LieEquiv.refl_symmCommRing · cited by 17173CommRingLieRing · cited by 1548LieRingLieAlgebra · cited by 1246LieAlgebraLieEquiv · cited by 86LieEquivLieEquiv.reflCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • CommRingstatement and proof · cited by 17,173
  • LieRingstatement and proof · cited by 1,548
  • LieAlgebrastatement and proof · cited by 1,246
  • LieEquivstatement · cited by 86

Cited by6

Results whose statement or proof uses this declaration.