hasRankNullity — Mathlib

English

If R is a domain, then HasRankNullity R holds; in particular, for every R-module M, rank-nullity decompositions exist (rank_quotient_add_rank and independent subset of M realizing rank).

Русский

Если R — область, то выполняется HasRankNullity R: существует разложение ранга-нулитити и существует подмножество, реализующее ранг.

LaTeX

$$$\text{HasRankNullity } R$$

Lean4

instance hasRankNullity [IsDomain R] : HasRankNullity.{w} R
    where
  rank_quotient_add_rank := rank_quotient_add_rank_of_isDomain
  exists_set_linearIndependent M := exists_set_linearIndependent_of_isDomain R M

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