Structures · Algebra
OrzechProperty
A ring R satisfies the Orzech property, if for any finitely generated R-module M,
any surjective homomorphism f : N → M from a submodule N of M to M is injective.
NOTE: In the definition we need to assume that M has the same universe level as R, but it
in fact implies the universe polymorphic versions
OrzechProperty.injective_of_surjective_of_injective
and OrzechProperty.injective_of_surjective_of_submodule.
- Defined in
- Mathlib.RingTheory.OrzechProperty
- Shape
- One type argument · adds injective_of_surjective_of_submodule'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- OrzechProperty.injective_of_surjective_of_injective
- linearIndependent_iff_card_eq_finrank_span
- linearIndependent_of_top_le_span_of_card_eq_finrank
- basisOfTopLeSpanOfCardEqFinrank
- coe_basisOfTopLeSpanOfCardEqFinrank
- OrzechProperty.injective_of_surjective_endomorphism
- linearIndependent_of_top_le_span_of_card_le_finrank
- setBasisOfTopLeSpanOfCardEqFinrank
- OrzechProperty.injective_of_surjective_of_submodule'
- OrzechProperty.bijective_of_surjective_of_finrank_le
- finsetBasisOfTopLeSpanOfCardEqFinrank
- OrzechProperty.bijective_of_surjective_of_injective
- finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply
- OrzechProperty.bijective_of_surjective_endomorphism
- setBasisOfTopLeSpanOfCardEqFinrank_repr_apply
- OrzechProperty.injective_of_surjective_of_submodule
- instIsStablyFiniteRingOfOrzechProperty
- basisOfTopLeSpanOfCardEqFinrank.congr_simp
- strongRankCondition_of_orzechProperty
- linearIndependent_iff_card_le_finrank_span
Ancestors0
No ancestors.