Theorems · Theorem · linear algebra

StrongRankCondition.of_isNoetherian

∀ {R : Type u} [inst : Semiring R] [Nontrivial R] [∀ (n : ℕ), IsNoetherian R (Fin n → R)], StrongRankCondition R

If each Rⁿ is a Noetherian R-module, then R satisfies the strong rank condition. Not an instance for performance reasons. If R is a ring, the assumption is equivalent to R being a left-Noetherian ring, but this is not necessarily the case for semirings: ℕ is a Noetherian semiring but ℕ² is not a Noetherian ℕ-module. (ℕ does satisfy the strong rank condition.)

Defined in

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringNontrivialIsNoetherian