sup_free_of_free — Mathlib

English

If A and B are linearly disjoint and free as R-modules, then A ⊔ B is a free R-module.

Русский

Если A и B линейно несовместны и свободны как модули над R, то A ⊔ B свободен как R-модуль.

LaTeX

$$$A \\text{ LinearDisjoint } B \\quad\\Rightarrow\\quad \\uparrow(A \\sqcup B) \\text{ is free over } R$$$

Lean4

/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint, and if they are free `R`-modules, then `A ⊔ B` is also a free `R`-module. -/
theorem sup_free_of_free [Module.Free R A] [Module.Free R B] : Module.Free R ↥(A ⊔ B) :=
  Module.Free.of_equiv H.mulMap.toLinearEquiv

Похожие утверждения