Documentation Verification Report

Orzech

📁 Source: Mathlib/RingTheory/Noetherian/Orzech.lean

Statistics

Metric	Count
Definitions `equivPUnitOfProdInjective`	1
Theorems `bijective_of_surjective_endomorphism`, `equivPUnitOfProdInjective_apply`, `equivPUnitOfProdInjective_symm_apply`, `injective_of_surjective_endomorphism`, `injective_of_surjective_of_injective`, `injective_of_surjective_of_submodule`, `subsingleton_of_prod_injective`, `orzechProperty`	8
Total	9

IsNoetherian

Definitions

Name	Category	Theorems
`equivPUnitOfProdInjective` 📖	CompOp	2 math math: `equivPUnitOfProdInjective_apply`, `equivPUnitOfProdInjective_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_surjective_endomorphism` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Function.Bijective`	—	`injective_of_surjective_endomorphism`
`equivPUnitOfProdInjective_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `PUnit.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `equivPUnitOfProdInjective`	—	`RingHomInvPair.ids`
`equivPUnitOfProdInjective_symm_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `PUnit.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `equivPUnitOfProdInjective` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`injective_of_surjective_endomorphism` 📖	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`injective_of_surjective_of_injective` `RingHomInvPair.ids` `LinearEquiv.injective`
`injective_of_surjective_of_injective` 📖	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`monotone_nat_of_le_succ` `LinearMap.iterateMapComap_le_succ` `RingHomSurjective.ids` `Submodule.map_bot` `monotone_stabilizes_iff_noetherian` `isNoetherian_of_injective` `LinearMap.ker_eq_bot` `bot_unique` `LinearMap.ker_le_of_iterateMapComap_eq_succ`
`injective_of_surjective_of_submodule` 📖	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `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`
`subsingleton_of_prod_injective` 📖	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike`	—	—	`injective_of_surjective_of_injective` `LinearMap.fst_surjective`

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orzechProperty` 📖	mathematical	—	`OrzechProperty` `Ring.toSemiring`	—	`IsNoetherian.injective_of_surjective_of_submodule` `isNoetherian_of_isNoetherianRing_of_finite`

---

← Back to Index