Loogle!

Result

Found 329 declarations mentioning LieIdeal. Of these, only the first 200 are shown.

• LieIdeal 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Type v
• LieIdeal.toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieSubalgebra R L
• instCoeLieIdealLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Coe (LieIdeal R L) (LieSubalgebra R L)
• LieHom.idealRange 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : LieIdeal R L'
• LieHom.ker 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : LieIdeal R L
• LieIdeal.comap 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') : LieIdeal R L
• LieIdeal.map 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) : LieIdeal R L'
• LieIdeal.lieRing 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieRing ↥I
• LieIdeal.bracket 📋 Mathlib.Algebra.Lie.Ideal
  (M : Type w) {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [Bracket L M] : Bracket (↥I) M
• LieIdeal.top_toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal.toLieSubalgebra R L ⊤ = ⊤
• LieIdeal.lieAlgebra 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra R ↥I
• LieIdeal.coe_toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑(LieIdeal.toLieSubalgebra R L I) = ↑I
• LieIdeal.toLieSubalgebra_toSubmodule 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : (LieIdeal.toLieSubalgebra R L I).toSubmodule = ↑I
• LieIdeal.lieRingModule 📋 Mathlib.Algebra.Lie.Ideal
  (M : Type w) [AddCommGroup M] {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] : LieRingModule (↥I) M
• LieIdeal.incl 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↥I →ₗ⁅R⁆ L
• LieHom.idealRange_eq_map 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : f.idealRange = LieIdeal.map f ⊤
• LieIdeal.incl_isIdealMorphism 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.IsIdealMorphism
• LieIdeal.mem_toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) : x ∈ LieIdeal.toLieSubalgebra R L I ↔ x ∈ I
• LieHom.idealRange_eq_lieSpan_range 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : f.idealRange = LieSubmodule.lieSpan R L' ↑f.range
• LieIdeal.incl_idealRange 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.idealRange = I
• LieHom.range_subset_idealRange 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : ↑f.range ⊆ ↑f.idealRange
• LieHom.ker_le_comap 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') : f.ker ≤ LieIdeal.comap f J
• LieHom.map_le_idealRange 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) : LieIdeal.map f I ≤ f.idealRange
• LieIdeal.comap_map_le 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : I ≤ LieIdeal.comap f (LieIdeal.map f I)
• LieIdeal.map_comap_le 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} : LieIdeal.map f (LieIdeal.comap f J) ≤ J
• instBracketSubtypeMemLieIdeal 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Bracket ↥I ↥I
• LieHom.idealRange_eq_top_of_surjective 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (h : Function.Surjective ⇑f) : f.idealRange = ⊤
• LieHom.ker_eq_bot 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : f.ker = ⊥ ↔ Function.Injective ⇑f
• LieHom.mem_idealRange 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (x : L) : f x ∈ f.idealRange
• LieIdeal.incl_range 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.range = LieIdeal.toLieSubalgebra R L I
• LieIdeal.map_sup_ker_eq_map 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I
• LieIdeal.comap_mono 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} : Monotone (LieIdeal.comap f)
• LieIdeal.map_mono 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} : Monotone (LieIdeal.map f)
• lie_mem_left 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : L) (h : x ∈ I) : ⁅x, y⁆ ∈ I
• lie_mem_right 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : L) (h : y ∈ I) : ⁅x, y⁆ ∈ I
• LieIdeal.map_comap_eq 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} (h : f.IsIdealMorphism) : LieIdeal.map f (LieIdeal.comap f J) = f.idealRange ⊓ J
• LieIdeal.map_sup_ker_eq_map' 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : LieIdeal.map f I ⊔ LieIdeal.map f f.ker = LieIdeal.map f I
• LieSubalgebra.exists_lieIdeal_coe_eq_iff 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : (∃ I, LieIdeal.toLieSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
• LieIdeal.gc_map_comap 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : GaloisConnection (LieIdeal.map f) (LieIdeal.comap f)
• instIsLieTowerSubtypeMemLieIdeal 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [LieRingModule L M] [LieAlgebra R L] (I : LieIdeal R L) : IsLieTower (↥I) L M
• LieHom.mem_idealRange_iff 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (h : f.IsIdealMorphism) {y : L'} : y ∈ f.idealRange ↔ ∃ x, f x = y
• LieIdeal.lieModule 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] (I : LieIdeal R L) : LieModule R (↥I) M
• LieHom.mem_ker 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {x : L} : x ∈ f.ker ↔ f x = 0
• LieIdeal.map_eq_bot_iff 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : LieIdeal.map f I = ⊥ ↔ I ≤ f.ker
• LieIdeal.map_sup 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I I₂ : LieIdeal R L} : LieIdeal.map f (I ⊔ I₂) = LieIdeal.map f I ⊔ LieIdeal.map f I₂
• LieIdeal.bot_of_map_eq_bot 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} (h₁ : Function.Injective ⇑f) (h₂ : LieIdeal.map f I = ⊥) : I = ⊥
• LieIdeal.mem_map 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {x : L} (hx : x ∈ I) : f x ∈ LieIdeal.map f I
• LieIdeal.subsingleton_of_bot 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Subsingleton (LieIdeal R ↥⊥)
• LieIdeal.mem_comap 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} {x : L} : x ∈ LieIdeal.comap f J ↔ f x ∈ J
• LieIdeal.map_of_image 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'} (h : ⇑f '' ↑I = ↑J) : LieIdeal.map f I = J
• LieIdeal.topEquiv 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ↥⊤ ≃ₗ⁅R⁆ L
• LieIdeal.map_le_iff_le_comap 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'} : LieIdeal.map f I ≤ J ↔ I ≤ LieIdeal.comap f J
• LieIdeal.comap_toSubmodule 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') : ↑(LieIdeal.comap f J) = Submodule.comap ↑f ↑J
• LieHom.le_ker_iff 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) : I ≤ f.ker ↔ ∀ x ∈ I, f x = 0
• LieIdeal.inclusion 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : ↥I₁ →ₗ⁅R⁆ ↥I₂
• LieIdeal.coe_bracket_of_module 📋 Mathlib.Algebra.Lie.Ideal
  (M : Type w) [AddCommGroup M] {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] (x : ↥I) (m : M) : ⁅x, m⁆ = ⁅↑x, m⁆
• LieIdeal.map_le 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (J : LieIdeal R L') : LieIdeal.map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J
• LieIdeal.coe_map_of_surjective 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} (h : Function.Surjective ⇑f) : ↑(LieIdeal.map f I) = Submodule.map ↑f ↑I
• LieIdeal.comap_map_eq 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} (h : ↑(LieIdeal.map f I) = ⇑f '' ↑I) : LieIdeal.comap f (LieIdeal.map f I) = I ⊔ f.ker
• instIsLieTowerSubtypeMemLieIdeal_1 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [LieRingModule L M] [LieAlgebra R L] (I : LieIdeal R L) : IsLieTower L (↥I) M
• LieIdeal.mem_map_of_surjective 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {y : L'} (h₁ : Function.Surjective ⇑f) (h₂ : y ∈ LieIdeal.map f I) : ∃ x, f ↑x = y
• LieIdeal.map_toSubmodule 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (h : ↑(LieIdeal.map f I) = ⇑f '' ↑I) : ↑(LieIdeal.map f I) = Submodule.map ↑f ↑I
• LieIdeal.incl_injective 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Function.Injective ⇑I.incl
• LieIdeal.incl_apply 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : ↥I) : I.incl x = ↑x
• LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff 📋 Mathlib.Algebra.Lie.Ideal
  (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {K' : LieSubalgebra R L} (h : K ≤ K') : (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
• LieIdeal.incl_coe 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑I.incl = (LieIdeal.toLieSubalgebra R L I).subtype
• LieIdeal.ker_incl 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.ker = ⊥
• LieIdeal.comap_incl_self 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieIdeal.comap I.incl I = ⊤
• LieIdeal.comap_incl_eq_top 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I I₂ : LieIdeal R L} : LieIdeal.comap I.incl I₂ = ⊤ ↔ I ≤ I₂
• LieIdeal.inclusion_injective 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : Function.Injective ⇑(LieIdeal.inclusion h)
• LieIdeal.coe_inclusion 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : ↥I₁) : ↑((LieIdeal.inclusion h) x) = ↑x
• LieIdeal.comap_incl_eq_bot 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I I₂ : LieIdeal R L} : LieIdeal.comap I.incl I₂ = ⊥ ↔ Disjoint I I₂
• LieIdeal.inclusion_apply 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : ↥I₁) : (LieIdeal.inclusion h) x = ⟨↑x, ⋯⟩
• LieIdeal.topEquiv_apply 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : ↥⊤) : LieIdeal.topEquiv x = ↑x
• LieSubmodule.hasBracket 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] : Bracket (LieIdeal R L) (LieSubmodule R L M)
• LieSubmodule.lie_le_left 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) : ⁅I, J⁆ ≤ I
• LieSubmodule.lie_comm 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) : ⁅I, J⁆ = ⁅J, I⁆
• LieSubmodule.lie_bot 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, ⊥⁆ = ⊥
• LieSubmodule.lie_le_right 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, N⁆ ≤ N
• LieSubmodule.bot_lie 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] : ⁅⊥, N⁆ = ⊥
• LieSubmodule.lie_le_inf 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) : ⁅I, J⁆ ≤ I ⊓ J
• LieIdeal.map_bracket_eq 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') {I₁ I₂ : LieIdeal R L} (h : Function.Surjective ⇑f) : LieIdeal.map f ⁅I₁, I₂⁆ = ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
• LieIdeal.comap_bracket_le 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') {J₁ J₂ : LieIdeal R L'} : ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ≤ LieIdeal.comap f ⁅J₁, J₂⁆
• LieIdeal.map_bracket_le 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') {I₁ I₂ : LieIdeal R L} : LieIdeal.map f ⁅I₁, I₂⁆ ≤ ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
• LieSubmodule.lie_mem_lie 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} [LieAlgebra R L] {I : LieIdeal R L} {x : L} {m : M} (hx : x ∈ I) (hm : m ∈ N) : ⁅x, m⁆ ∈ ⁅I, N⁆
• LieSubmodule.lie_sup 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆
• LieSubmodule.mono_lie_left 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] {I J : LieIdeal R L} (h : I ≤ J) : ⁅I, N⁆ ≤ ⁅J, N⁆
• LieIdeal.map_comap_incl 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} : LieIdeal.map I₁.incl (LieIdeal.comap I₁.incl I₂) = I₁ ⊓ I₂
• LieSubmodule.mono_lie_right 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} [LieAlgebra R L] (I : LieIdeal R L) (h : N ≤ N') : ⁅I, N⁆ ≤ ⁅I, N'⁆
• LieSubmodule.sup_lie 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I J : LieIdeal R L) : ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
• LieSubmodule.map_bracket_eq 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂) [LieAlgebra R L] [LieModule R L M₂] (I : LieIdeal R L) [LieModule R L M] : LieSubmodule.map f ⁅I, N⁆ = ⁅I, LieSubmodule.map f N⁆
• LieSubmodule.lie_eq_bot_iff 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
• LieSubmodule.lieIdeal_oper_eq_linear_span' 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) [LieModule R L M] : ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
• LieSubmodule.lie_inf 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆
• LieSubmodule.inf_lie 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I J : LieIdeal R L) : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆
• LieIdeal.map_comap_bracket_eq 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) : LieIdeal.map f ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆
• LieSubmodule.lie_le_iff 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
• LieSubmodule.mono_lie 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} [LieAlgebra R L] {I J : LieIdeal R L} (h₁ : I ≤ J) (h₂ : N ≤ N') : ⁅I, N⁆ ≤ ⁅J, N'⁆
• LieIdeal.comap_bracket_eq 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) : LieIdeal.comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ⊔ f.ker
• LieSubmodule.lie_coe_mem_lie 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} [LieAlgebra R L] {I : LieIdeal R L} (x : ↥I) (m : ↥N) : ⁅↑x, ↑m⁆ ∈ ⁅I, N⁆
• LieSubmodule.comap_bracket_eq 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂) [LieAlgebra R L] [LieModule R L M₂] (I : LieIdeal R L) [LieModule R L M] (hf₁ : f.ker = ⊥) (hf₂ : N₂ ≤ f.range) : LieSubmodule.comap f ⁅I, N₂⁆ = ⁅I, LieSubmodule.comap f N₂⁆
• LieSubmodule.lieIdeal_oper_eq_span 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) : ⁅I, N⁆ = LieSubmodule.lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
• LieSubmodule.lieIdeal_oper_eq_linear_span 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (I : LieIdeal R L) [LieModule R L M] : ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
• LieIdeal.comap_bracket_incl 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {I₁ I₂ : LieIdeal R L} : ⁅LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂⁆ = LieIdeal.comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
• LieIdeal.comap_bracket_incl_of_le 📋 Mathlib.Algebra.Lie.IdealOperations
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {I₁ I₂ : LieIdeal R L} (h₁ : I₁ ≤ I) (h₂ : I₂ ≤ I) : ⁅LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂⁆ = LieIdeal.comap I.incl ⁅I₁, I₂⁆
• LieAlgebra.center 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal R L
• LieModule.ker 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieIdeal R L
• LieAlgebra.self_module_ker_eq_center 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieModule.ker R L L = LieAlgebra.center R L
• LieAlgebra.center_eq_bot 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieModule.IsFaithful R L L] : LieAlgebra.center R L = ⊥
• LieAlgebra.isFaithful_self_iff 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieModule.IsFaithful R L L ↔ LieAlgebra.center R L = ⊥
• LieAlgebra.isLieAbelian_iff_center_eq_top 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : IsLieAbelian L ↔ LieAlgebra.center R L = ⊤
• LieModule.ker_eq_bot 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsFaithful R L M] : LieModule.ker R L M = ⊥
• LieModule.isFaithful_iff_ker_eq_bot 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.IsFaithful R L M ↔ LieModule.ker R L M = ⊥
• LieModule.ideal_oper_maxTrivSubmodule_eq_bot 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) : ⁅I, LieModule.maxTrivSubmodule R L M⁆ = ⊥
• LieModule.mem_ker 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0
• LieSubmodule.trivial_lie_oper_zero 📋 Mathlib.Algebra.Lie.Abelian
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (I : LieIdeal R L) [LieModule.IsTrivial L M] : ⁅I, N⁆ = ⊥
• LieModule.le_max_triv_iff_bracket_eq_bot 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} : N ≤ LieModule.maxTrivSubmodule R L M ↔ ⁅⊤, N⁆ = ⊥
• LieAlgebra.instIsLieAbelianSubtypeMemLieIdealCenter 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : IsLieAbelian ↥(LieAlgebra.center R L)
• lie_eq_self_of_isAtom_of_ne_bot 📋 Mathlib.Algebra.Lie.Abelian
  {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {I : LieIdeal R L} (hN : IsAtom N) (h : ⁅I, N⁆ ≠ ⊥) : ⁅I, N⁆ = N
• LieAlgebra.abelian_of_le_center 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (h : I ≤ LieAlgebra.center R L) : IsLieAbelian ↥I
• LieSubmodule.lie_abelian_iff_lie_self_eq_bot 📋 Mathlib.Algebra.Lie.Abelian
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsLieAbelian ↥I ↔ ⁅I, I⁆ = ⊥
• LieAlgebra.ad_ker_eq_self_module_ker 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : (LieAlgebra.ad R L).ker = LieModule.ker R L L
• lie_eq_self_of_isAtom_of_nonabelian 📋 Mathlib.Algebra.Lie.Abelian
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (hI : IsAtom I) (h : ¬IsLieAbelian ↥I) : ⁅I, I⁆ = I
• LieIdeal.isLieAbelian_iff 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} : IsLieAbelian ↥I ↔ I ≤ LieModule.ker R L ↥I
• LieIdeal.isLieAbelian_of_trivial 📋 Mathlib.Algebra.Lie.Abelian
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [h : LieModule.IsTrivial L ↥I] : IsLieAbelian ↥I
• LieModule.commute_toEnd_of_mem_center_left 📋 Mathlib.Algebra.Lie.Abelian
  {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} (hx : x ∈ LieAlgebra.center R L) (y : L) : Commute ((LieModule.toEnd R L M) x) ((LieModule.toEnd R L M) y)
• LieModule.commute_toEnd_of_mem_center_right 📋 Mathlib.Algebra.Lie.Abelian
  {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} (hx : x ∈ LieAlgebra.center R L) (y : L) : Commute ((LieModule.toEnd R L M) y) ((LieModule.toEnd R L M) x)
• LieDerivation.ad_ker_eq_center 📋 Mathlib.Algebra.Lie.AdjointAction.Derivation
  (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : (LieDerivation.ad R L).ker = LieAlgebra.center R L
• LieDerivation.injective_ad_of_center_eq_bot 📋 Mathlib.Algebra.Lie.AdjointAction.Derivation
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (h : LieAlgebra.center R L = ⊥) : Function.Injective ⇑(LieDerivation.ad R L)
• LieDerivation.mem_ad_idealRange_iff 📋 Mathlib.Algebra.Lie.AdjointAction.Derivation
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {D : LieDerivation R L L} : D ∈ (LieDerivation.ad R L).idealRange ↔ ∃ x, (LieDerivation.ad R L) x = D
• LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot 📋 Mathlib.Algebra.Lie.AdjointAction.Derivation
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (h : LieAlgebra.center R L = ⊥) : LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥
• LieSubmodule.lieIdeal_oper_eq_tensor_map_range 📋 Mathlib.Algebra.Lie.TensorProduct
  {R : Type u} [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (N : LieSubmodule R L M) : ⁅I, N⁆ = ((LieModule.toModuleHom R L M).comp (TensorProduct.LieModule.mapIncl I N)).range
• LieSubmodule.lie_baseChange 📋 Mathlib.Algebra.Lie.BaseChange
  (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] {I : LieIdeal R L} {N : LieSubmodule R L M} : LieSubmodule.baseChange A ⁅I, N⁆ = ⁅LieSubmodule.baseChange A I, LieSubmodule.baseChange A N⁆
• LieAlgebra.radical 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal R L
• LieAlgebra.derivedLengthOfIdeal 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ℕ
• LieAlgebra.derivedSeries 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieIdeal R L
• LieAlgebra.derivedAbelianOfIdeal 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieIdeal R L
• LieAlgebra.derivedSeriesOfIdeal 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieIdeal R L → LieIdeal R L
• LieAlgebra.derivedSeriesOfIdeal_zero 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra.derivedSeriesOfIdeal R L 0 I = I
• LieAlgebra.radical_eq_top_of_isSolvable 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable L] : LieAlgebra.radical R L = ⊤
• LieAlgebra.IsSolvable.mk 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {k : ℕ} (h : LieAlgebra.derivedSeries R L k = ⊥) : LieAlgebra.IsSolvable L
• LieAlgebra.IsSolvable.mk_int 📋 Mathlib.Algebra.Lie.Solvable
  {L : Type v} [LieRing L] (solvable_int : ∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥) : LieAlgebra.IsSolvable L
• LieAlgebra.IsSolvable.solvable 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable L] : ∃ k, LieAlgebra.derivedSeries R L k = ⊥
• LieAlgebra.IsSolvable.solvable_int 📋 Mathlib.Algebra.Lie.Solvable
  {L : Type v} {inst✝ : LieRing L} [self : LieAlgebra.IsSolvable L] : ∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥
• LieAlgebra.derivedSeriesOfIdeal_add 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k l : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + l) I = LieAlgebra.derivedSeriesOfIdeal R L k (LieAlgebra.derivedSeriesOfIdeal R L l I)
• LieAlgebra.isSolvable_iff 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.IsSolvable L ↔ ∃ k, LieAlgebra.derivedSeries R L k = ⊥
• LieAlgebra.isSolvable_iff_int 📋 Mathlib.Algebra.Lie.Solvable
  (L : Type v) [LieRing L] : LieAlgebra.IsSolvable L ↔ ∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥
• LieAlgebra.derivedSeries_def 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieAlgebra.derivedSeries R L k = LieAlgebra.derivedSeriesOfIdeal R L k ⊤
• LieAlgebra.center_le_radical 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.center R L ≤ LieAlgebra.radical R L
• LieAlgebra.derivedSeriesOfIdeal_le_self 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ I
• Function.instIsSolvableSubtypeMemLieIdeal 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A : LieIdeal R L) [LieAlgebra.IsSolvable L] : LieAlgebra.IsSolvable ↥A
• LieAlgebra.instUniqueSubtypeMemLieIdealBot 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Unique ↥⊥
• LieAlgebra.derivedSeries_of_bot_eq_bot 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L k ⊥ = ⊥
• LieAlgebra.derivedSeriesOfIdeal_antitone 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {k l : ℕ} (h : l ≤ k) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l I
• LieAlgebra.derivedLength_eq_derivedLengthOfIdeal 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra.derivedLength R ↥I = LieAlgebra.derivedLengthOfIdeal R L I
• LieAlgebra.derivedSeriesOfIdeal_succ_le 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I ≤ LieAlgebra.derivedSeriesOfIdeal R L k I
• LieIdeal.derivedSeries_map_eq 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} (k : ℕ) (h : Function.Surjective ⇑f) : LieIdeal.map f (LieAlgebra.derivedSeries R L' k) = LieAlgebra.derivedSeries R L k
• LieAlgebra.radicalIsSolvable 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieAlgebra.IsSolvable ↥(LieAlgebra.radical R L)
• LieIdeal.coe_derivedSeries_eq_int 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : ↑(LieAlgebra.derivedSeries R L k) = ↑(LieAlgebra.derivedSeries ℤ L k)
• LieAlgebra.derivedSeries_lt_top_of_solvable 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable L] [Nontrivial L] : LieAlgebra.derivedSeries R L 1 < ⊤
• LieIdeal.derivedSeries_map_le 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} (k : ℕ) : LieIdeal.map f (LieAlgebra.derivedSeries R L' k) ≤ LieAlgebra.derivedSeries R L k
• LieAlgebra.derivedSeriesOfIdeal_succ 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⁅LieAlgebra.derivedSeriesOfIdeal R L k I, LieAlgebra.derivedSeriesOfIdeal R L k I⁆
• LieIdeal.derivedSeries_eq_top 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (h : LieAlgebra.derivedSeries R L 1 = ⊤) : LieAlgebra.derivedSeries R L n = ⊤
• LieAlgebra.isSolvableBot 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.IsSolvable ↥⊥
• LieIdeal.derivedSeries_succ_eq_top_iff 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : LieAlgebra.derivedSeries R L (n + 1) = ⊤ ↔ LieAlgebra.derivedSeries R L 1 = ⊤
• LieAlgebra.derivedLength_zero 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieAlgebra.IsSolvable ↥I] : LieAlgebra.derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
• LieAlgebra.derivedSeriesOfIdeal_mono 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : I ≤ J) (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L k J
• LieAlgebra.derivedSeriesOfIdeal_le 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} {k l : ℕ} (h₁ : I ≤ J) (h₂ : l ≤ k) : LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l J
• LieAlgebra.LieIdeal.solvable_iff_le_radical 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) : LieAlgebra.IsSolvable ↥I ↔ I ≤ LieAlgebra.radical R L
• LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [h : LieAlgebra.IsSolvable ↥I] : LieAlgebra.derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥
• LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieIdeal.map I.incl (LieAlgebra.derivedSeries R (↥I) k) = LieAlgebra.derivedSeriesOfIdeal R L k I
• LieAlgebra.le_solvable_ideal_solvable 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h₁ : I ≤ J) : LieAlgebra.IsSolvable ↥J → LieAlgebra.IsSolvable ↥I
• LieAlgebra.derivedSeries_baseChange 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u_1} [CommRing A] [Algebra R A] (k : ℕ) : LieAlgebra.derivedSeries A (TensorProduct R A L) k = LieSubmodule.baseChange A (LieAlgebra.derivedSeries R L k)
• LieAlgebra.derivedSeriesOfIdeal_add_le_add 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (k l : ℕ) : LieAlgebra.derivedSeriesOfIdeal R L (k + l) (I + J) ≤ LieAlgebra.derivedSeriesOfIdeal R L k I + LieAlgebra.derivedSeriesOfIdeal R L l J
• LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeries R (↥I) k = LieIdeal.comap I.incl (LieAlgebra.derivedSeriesOfIdeal R L k I)
• LieAlgebra.abelian_derivedAbelianOfIdeal 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsLieAbelian ↥(LieAlgebra.derivedAbelianOfIdeal I)
• LieAlgebra.derivedSeriesOfIdeal_baseChange 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {A : Type u_1} [CommRing A] [Algebra R A] (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal A (TensorProduct R A L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (LieAlgebra.derivedSeriesOfIdeal R L k I)
• LieAlgebra.abelian_iff_derived_one_eq_bot 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsLieAbelian ↥I ↔ LieAlgebra.derivedSeriesOfIdeal R L 1 I = ⊥
• LieAlgebra.isSolvableAdd 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} [LieAlgebra.IsSolvable ↥I] [LieAlgebra.IsSolvable ↥J] : LieAlgebra.IsSolvable ↥(I + J)
• LieAlgebra.abelian_iff_derived_succ_eq_bot 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : IsLieAbelian ↥(LieAlgebra.derivedSeriesOfIdeal R L k I) ↔ LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⊥
• LieAlgebra.derivedSeries_of_derivedLength_succ 📋 Mathlib.Algebra.Lie.Solvable
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedLengthOfIdeal R L I = k + 1 ↔ IsLieAbelian ↥(LieAlgebra.derivedSeriesOfIdeal R L k I) ∧ LieAlgebra.derivedSeriesOfIdeal R L k I ≠ ⊥
• LieIdeal.derivedSeries_eq_bot_iff 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : LieAlgebra.derivedSeries R (↥I) k = ⊥ ↔ LieAlgebra.derivedSeriesOfIdeal R L k I = ⊥
• LieIdeal.derivedSeries_add_eq_bot 📋 Mathlib.Algebra.Lie.Solvable
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {k l : ℕ} {I J : LieIdeal R L} (hI : LieAlgebra.derivedSeries R (↥I) k = ⊥) (hJ : LieAlgebra.derivedSeries R (↥J) l = ⊥) : LieAlgebra.derivedSeries R (↥(I + J)) (k + l) = ⊥
• LieSubmodule.Quotient.lieQuotientLieRing 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieRing (L ⧸ I)
• LieSubmodule.Quotient.lieQuotientLieAlgebra 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra R (L ⧸ I)
• LieSubmodule.Quotient.lieQuotientHasBracket 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Bracket (L ⧸ I) (L ⧸ I)
• LieHom.quotKerEquivRange 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : (L ⧸ f.ker) ≃ₗ⁅R⁆ ↥f.range
• LieSubmodule.Quotient.mk_bracket 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : L) : LieSubmodule.Quotient.mk ⁅x, y⁆ = ⁅LieSubmodule.Quotient.mk x, LieSubmodule.Quotient.mk y⁆
• LieHom.quotKerEquivRange_invFun 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a✝ : ↥(↑f).range) : f.quotKerEquivRange.invFun a✝ = (↑f).quotKerEquivRange.invFun a✝
• LieHom.quotKerEquivRange_toFun 📋 Mathlib.Algebra.Lie.Quotient
  {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a : L ⧸ (↑f).ker) : f.quotKerEquivRange a = (↑f).quotKerEquivRange a
• LieSubmodule.idealizer 📋 Mathlib.Algebra.Lie.Normalizer
  {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) : LieIdeal R L
• LieIdeal.idealizer_eq_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieSubmodule.idealizer I = LieSubmodule.normalizer I
• LieSubmodule.mem_idealizer 📋 Mathlib.Algebra.Lie.Normalizer
  {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) {x : L} : x ∈ N.idealizer ↔ ∀ (m : M), ⁅x, m⁆ ∈ N
• LieSubmodule.gc_top_lie_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
  {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : GaloisConnection (fun N => ⁅⊤, N⁆) LieSubmodule.normalizer
• LieSubmodule.top_lie_le_iff_le_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
  {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N N' : LieSubmodule R L M) : ⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer
• LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H K : LieSubalgebra R L} (h₁ : H ≤ K) (h₂ : K ≤ H.normalizer) : ∃ I, LieIdeal.toLieSubalgebra R (↥K) I = LieSubalgebra.ofLe h₁
• LieIdeal.lcs 📋 Mathlib.Algebra.Lie.Nilpotent
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : LieSubmodule R L M
• LieAlgebra.non_trivial_center_of_isNilpotent 📋 Mathlib.Algebra.Lie.Nilpotent
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial L] [LieRing.IsNilpotent L] : Nontrivial ↥(LieAlgebra.center R L)
• LieAlgebra.center_le_maxNilpotentIdeal 📋 Mathlib.Algebra.Lie.Nilpotent
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.center R L ≤ LieAlgebra.maxNilpotentIdeal R L
• LieModule.derivedSeries_le_lowerCentralSeries 📋 Mathlib.Algebra.Lie.Nilpotent
  (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieAlgebra.derivedSeries R L k ≤ LieModule.lowerCentralSeries R L L k

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59