Theorems · Theorem · linear algebra

CommSemiring.rank_self

∀ (R : Type u_1) [inst : CommSemiring R], Module.rank R R = 1

TODO: prove that nontrivial commutative semirings satisfy the strong rank condition, following Free sets and free subsemimodules in a semimodule by Yi-Jia Tan, Theorem 3.2. Rings R that fail the strong rank condition but satisfy rank R R = 1 are expected to exist, see https://mathoverflow.net/questions/317422/rings-that-fail-to-satisfy-the-strong-rank-condition.

Defined in

Mathlib.LinearAlgebra.Dimension.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiring