theorem LieAlgebra.isKilling_iff_killingCompl_top_eq_bot (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] : IsKilling R L ↔ LieIdeal.killingCompl R L ⊤ = ⊥

theorem LieAlgebra.isKilling_iff_nondegenerate_killingForm {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : IsKilling R L ↔ (killingForm R L).Nondegenerate

theorem LieIdeal.toSubmodule_killingCompl_eq_orthogonalBilin {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑(killingCompl R L I) = Submodule.orthogonalBilin (killingForm R L) ↑I

{name}BilinForm.orthogonal と {name}Submodule.orthogonalBilin で重複があってややこしい。 統合したい。

theorem LieIdeal.killingCompl_sup {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) : killingCompl R L (I ⊔ J) = killingCompl R L I ⊓ killingCompl R L J

theorem LieIdeal.isKilling_iff_isCompl_killingForm {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {I : LieIdeal K L} : LieAlgebra.IsKilling K ↥I ↔ IsCompl I (killingCompl K L I)

theorem LieIdeal.isKilling_iff_disjoint_killingForm {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {I : LieIdeal K L} : LieAlgebra.IsKilling K ↥I ↔ Disjoint I (killingCompl K L I)

instance LieIdeal.instIsKillingSubtypeMem_ado {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (I : LieIdeal K L) [LieAlgebra.IsKilling K L] : LieAlgebra.IsKilling K ↥I