OrzechProperty

📁 Source: Mathlib/RingTheory/OrzechProperty.lean

Statistics

Metric	Count
Definitions OrzechProperty	1
Theorems bijective_of_surjective_endomorphism, injective_of_surjective_endomorphism, injective_of_surjective_of_injective, injective_of_surjective_of_submodule, injective_of_surjective_of_submodule', instOfFinite, orzechProperty_iff	7
Total	8

OrzechProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_of_surjective_endomorphism 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Function.Bijective	—	injective_of_surjective_endomorphism
injective_of_surjective_endomorphism 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—	injective_of_surjective_of_injective RingHomInvPair.ids LinearEquiv.injective
injective_of_surjective_of_injective 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—	Module.Finite.exists_fin' RingHomInvPair.ids small_of_surjective small_Pi UnivLE.small univLE_of_max UnivLE.self RingHomCompTriple.ids EquivLike.toEmbeddingLike RingHomSurjective.invPair injective_of_surjective_of_submodule' Module.Finite.equiv
injective_of_surjective_of_submodule 📖	—	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike	—	—	injective_of_surjective_of_injective Submodule.injective_subtype
injective_of_surjective_of_submodule' 📖	—	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike	—	—	—
instOfFinite 📖	mathematical	—	OrzechProperty	—	Module.finite_of_finite Function.Injective.hasLeftInverse Submodule.subtype_injective Function.Injective.of_comp Function.Surjective.bijective_of_finite Subtype.finite Function.LeftInverse.surjective

(root)

Definitions

Name	Category	Theorems
OrzechProperty 📖	CompData	4 math math: OrzechProperty.instOfFinite, orzechProperty_iff, CommRing.orzechProperty, IsNoetherianRing.orzechProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orzechProperty_iff 📖	mathematical	—	OrzechProperty Submodule SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike	—	—

---

← Back to Index