commRing_strongRankCondition

Mathlib.LinearAlgebra.FreeModule.StrongRankCondition

URI: https://scilib.ai/kg/mathlib#commRing_strongRankCondition

← MathLib Explorer

English

Every nontrivial commutative ring satisfies the Strong Rank Condition.

Русский

Каждое ненулевое коммутативное кольцо удовлетворяет условию Strong Rank.

LaTeX

$$$\\text{StrongRankCondition } R$$$

Lean4

/-- Any nontrivial commutative ring satisfies the `StrongRankCondition`. -/
instance (priority := 100) commRing_strongRankCondition : StrongRankCondition R :=
  inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru