rank_inf_eq_one_of_flat_of_inj — Mathlib

English

If A,B are linearly disjoint and A is flat, then for any injection from R to S, rank(A∩B)=1.

Русский

Если A и B линейно раздельны и A плоская, то ранг A∩B равен 1 для любой инъекции из R в S.

LaTeX

$$$A \\perp_L B \\land \\mathrm{Flat}_R(A) \\Rightarrow \\mathrm{rank}_R(A\\cap B)=1$$$

Lean4

theorem rank_inf_eq_one_of_flat_of_inj (hf : Module.Flat R A ∨ Module.Flat R B)
    (hinj : Function.Injective (algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1 :=
  H.rank_inf_eq_one_of_commute_of_flat_of_inj hf (fun _ _ ↦ mul_comm _ _) hinj

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