English
If A ⊥ B and B is flat, then any R-linearly independent family in A remains independent after viewing in B.
Русский
Если A ⊥ B и B плоско над R, то любая R-линейно независимая семейство в A остаётся независимой при рассмотрении в B.
LaTeX
$$$A \\perp_L B\\;\\land\\; \\mathrm{Flat}_R(B) \\Rightarrow (a_i) \\subset A, \\ (\mathrm{LinearIndependent}_R(a_i)) \\Rightarrow \\mathrm{LinearIndependent}_B(A\\cdot a_i)$$$
Lean4
/-- In a commutative ring, if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module,
then for any family of `R`-linearly independent elements of `A`,
they are also `B`-linearly independent. -/
theorem linearIndependent_left_of_flat (H : A.LinearDisjoint B) [Module.Flat R B] {ι : Type*} {a : ι → A}
(ha : LinearIndependent R a) : LinearIndependent B (A.val ∘ a) :=
H.linearIndependent_left_of_flat_of_commute ha fun _ _ ↦ mul_comm _ _
