Structures · Data types
IsStablyFiniteRing
A semiring is stably finite if every matrix ring over it is Dedekind-finite.
- Defined in
- Mathlib.Data.Matrix.Mul
- Shape
- One type argument · adds isDedekindFiniteMonoid
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Matrix
- Module.End
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- Matrix.mul_eq_one_comm_of_equiv
- IsStablyFiniteRing.of_injective
- instIsStablyFiniteRingMulOpposite
- Matrix.instIsStablyFiniteRing
- Matrix.instIsDedekindFiniteMonoidOfIsStablyFiniteRing
- IsStablyFiniteRing.isDedekindFiniteMonoid
- instIsDedekindFiniteMonoidOfIsStablyFiniteRing
- instRankConditionOfIsStablyFiniteRingOfNontrivial
- instIsStablyFiniteRingSubtypeMem
- Module.End.injective_of_surjective_fin
- Matrix.mul_eq_one_comm_of_card_eq
- instIsStablyFiniteRingEndForallOfFinite
- LinearMap.comp_eq_id_comm
- Module.End.injective_of_surjective
- LinearMap.instIsStablyFiniteRingEnd
Ancestors0
No ancestors.