English
Every nontrivial commutative ring has invariant basis number.
Русский
Любое нетривиальное коммутативное кольцо имеет инвариантную базисную размерность.
LaTeX
$$For all R, if R is Commutative Ring and Nontrivial, then InvariantBasisNumber R.$$
Lean4
/-- Nontrivial commutative rings have the invariant basis number property.
There are two stronger results in mathlib: `commRing_strongRankCondition`, which says that any
nontrivial commutative ring satisfies the strong rank condition, and
`rankCondition_of_nontrivial_of_commSemiring`, which says that any nontrivial commutative semiring
satisfies the rank condition.
We prove this instance separately to avoid dependency on
`Mathlib/LinearAlgebra/Charpoly/Basic.lean` or `Mathlib/LinearAlgebra/Matrix/ToLin.lean`. -/
instance (priority := 100) invariantBasisNumber_of_nontrivial_of_commRing {R : Type u} [CommRing R] [Nontrivial R] :
InvariantBasisNumber R :=
⟨fun e =>
let ⟨I, _hI⟩ := Ideal.exists_maximal R
eq_of_fin_equiv (R ⧸ I) ((Ideal.piQuotEquiv _ _).symm ≪≫ₗ inducedEquiv _ e ≪≫ₗ Ideal.piQuotEquiv _ _)⟩
