Mathlib Map

Theorems · Theorem · linear algebra

IsStablyFiniteRing.of_injective

∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F),
  Function.Injective ⇑f → ∀ [IsStablyFiniteRing S], IsStablyFiniteRing R
Defined in
Mathlib.Data.Matrix.Mul
Cited by
1 results in Mathlib
Foundations
Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NonAssocSemiringNonAssocSemiringFunLikeRingHomClassIsStablyFiniteRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

RingEquiv.isStablyFiniteRing_iff · cited by 0RingEquiv.isStablyFiniteR…DFunLike.coe · cited by 62936DFunLike.coeMatrix · cited by 4303MatrixMonoidHom · cited by 3629MonoidHomFunLike · cited by 2560FunLikemap_zero · cited by 1614map_zeromap_one · cited by 861map_oneNonAssocSemiring · cited by 805NonAssocSemiringMatrix.map · cited by 247Matrix.mapRingHomClass · cited by 193RingHomClassMatrix.map_one · cited by 15Matrix.map_oneIsStablyFiniteRing · cited by 11IsStablyFiniteRingMatrix.map_mul · cited by 9Matrix.map_mulMatrix.map_injective · cited by 5Matrix.map_injectiveIsDedekindFiniteMonoid.of_injective · cited by 3IsDedekindFiniteMonoid.of…IsStablyFiniteRing.of_injecti…CITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.