rank_eq_one_of_commute_of_flat_of_self_of_inj

English

If A is linearly disjoint from itself and injective, then rank of A is 1.

Русский

Если A линейно несовместим с самим собой и инъективна, то ранг A равен 1.

LaTeX

$$$H: A \\perp_L A \\Rightarrow \\mathrm{rank}_R(A)=1$$$

Lean4

theorem rank_eq_one_of_commute_of_flat_of_self_of_inj (H : A.LinearDisjoint A) [Module.Flat R A]
    (hc : ∀ (a b : A), Commute a.1 b.1) (hinj : Function.Injective (algebraMap R S)) : Module.rank R A = 1 :=
  by
  rw [← inf_of_le_left (le_refl A)] at hc ⊢
  exact H.rank_inf_eq_one_of_commute_of_flat_left_of_inj hc hinj

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