theorem LieSubmodule.baseChange_injective (R : Type u_1) (A : Type u_2) (L : Type u_4) (M : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.FaithfullyFlat R A] : Function.Injective (baseChange A)

@[simp]

theorem LieSubmodule.baseChange_inj {R : Type u_1} {A : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.FaithfullyFlat R A] (I J : LieSubmodule R L M) : baseChange A I = baseChange A J ↔ I = J

@[simp]

theorem LieIdeal.lcs_baseChange {R : Type u_1} (A : Type u_3) {L : Type u_2} (M : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (n : ℕ) : lcs (LieSubmodule.baseChange A I) (TensorProduct R A M) n = LieSubmodule.baseChange A (I.lcs M n)