nontrivial_of_hasRankNullity

Mathlib.LinearAlgebra.Dimension.RankNullity

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

← MathLib Explorer

English

From HasRankNullity, a nontrivial ring exists: R is not the zero ring.

Русский

Из HasRankNullity следует, что R не нуль-кольцо (не ноль).

LaTeX

$$$ \operatorname{Nontrivial} R $$$

Lean4

theorem nontrivial_of_hasRankNullity : Nontrivial R :=
  by
  refine (subsingleton_or_nontrivial R).resolve_left fun H ↦ ?_
  have := rank_quotient_add_rank (R := R) (M := PUnit) ⊥
  simp [one_add_one_eq_two] at this

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

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

Разделы

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

Аффилиация

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