English
Any nontrivial ring with Orzech property satisfies the strong rank condition.
Русский
Любое ненулевое кольцо с свойством Орежа удовлетворяет сильному условию ранга.
LaTeX
$$$\text{StrongRankCondition } R\; \text{if and only if } (\text{OrzechProperty } R) \Rightarrow \text{RankCondition } R.$$$
Lean4
/-- Any nontrivial ring satisfying Orzech property also satisfies strong rank condition. -/
instance (priority := 100) strongRankCondition_of_orzechProperty [Nontrivial R] [OrzechProperty R] :
StrongRankCondition R := by
refine (strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_
let f : (Fin (n + 1) → R) →ₗ[R] Fin n → R :=
{ toFun := fun x ↦ x ∘ Fin.castSucc
map_add' := fun _ _ ↦ rfl
map_smul' := fun _ _ ↦ rfl }
have h : (0 : Fin (n + 1) → R) = update (0 : Fin (n + 1) → R) (Fin.last n) 1 :=
by
apply OrzechProperty.injective_of_surjective_of_injective i f hi (Fin.castSucc_injective _).surjective_comp_right
ext m
simp [f]
simpa using congr_fun h (Fin.last n)
