@[simp]

theorem LieSubalgebra.toSubmodule_sup_lieIdeal {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (I : LieIdeal R L) : (L' ⊔ ↑R L I).toSubmodule = L'.toSubmodule ⊔ ↑I

@[simp]

theorem LieIdeal.toLieSubalgebra_le_toLieSubalgebra {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I I' : LieIdeal R L) : ↑R L I ≤ ↑R L I' ↔ I ≤ I'

@[simp]

theorem LieIdeal.toLieSubalgebra_sup {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I I' : LieIdeal R L) : ↑R L (I ⊔ I') = ↑R L I ⊔ ↑R L I'

@[simp]

theorem LieIdeal.toLieSubalgebra_comap {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₂) (I : LieIdeal R L₂) : ↑R L (comap f I) = LieSubalgebra.comap f (↑R L₂ I)

theorem LieIdeal.toEnd_eq {R : Type u_1} {L : Type u_2} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) {x : ↥I} : (LieModule.toEnd R (↥I) M) x = (LieModule.toEnd R L M) ↑x

@[simp]

theorem LieIdeal.toEnd_mk {R : Type u_1} {L : Type u_2} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) {x : L} (hx : x ∈ I) : (LieModule.toEnd R (↥I) M) ⟨x, hx⟩ = (LieModule.toEnd R L M) x

theorem LieIdeal.image_eq_map_iff_exists_lieIdeal_toLieSubalgebra_eq_map {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₂) (I : LieIdeal R L) : ⇑f '' ↑I = ↑(map f I) ↔ ∃ (J : LieIdeal R L₂), ↑R L₂ J = LieSubalgebra.map f (↑R L I)