Documentation Verification Report

Injective

📁 Source: Mathlib/Algebra/Module/Injective.lean

Statistics

Metric	Count
Definitions `Baer`, `ExtensionOf`, `inhabited`, `max`, `toLinearPMap`, `extendIdealTo`, `extensionToFun`, `fst`, `ideal`, `idealTo`, `snd`, `extensionOfMax`, `extensionOfMaxAdjoin`, `instMinExtensionOf`, `instPartialOrderExtensionOf`, `instSemilatticeInfExtensionOf`, `supExtensionOfMaxSingleton`, `Injective`	18
Theorems `dExt`, `dExt_iff`, `ext`, `is_extension`, `le`, `le_max`, `toLinearPMap_injective`, `eqn`, `extendIdealTo_eq`, `extendIdealTo_is_extension`, `extendIdealTo_wd`, `extendIdealTo_wd'`, `extensionToFun_wd`, `chain_linearPMap_of_chain_extensionOf`, `extensionOfMax_is_max`, `extensionOfMax_le`, `extensionOfMax_to_submodule_eq_top`, `extension_property`, `extension_property_addMonoidHom`, `iff_injective`, `injective`, `of_equiv`, `of_injective`, `extension_property`, `out`, `pi`, `injective_iff`, `injective_iff_ulift_injective`, `injective_of_ulift_injective`, `ulift_injective_of_injective`	30
Total	48

Module

Definitions

Name	Category	Theorems
`Baer` 📖	MathDef	5 math math: `Baer.iff_injective`, `Baer.of_injective`, `Baer.of_divisible`, `Baer.congr`, `Flat.iff_characterModule_baer`
`Injective` 📖	CompData	12 math math: `ulift_injective_of_injective`, `Baer.injective`, `Baer.iff_injective`, `injective_of_ulift_injective`, `injective_iff_injective_object`, `injective_module_of_injective_object`, `injective_iff_ulift_injective`, `injective_of_semisimple_ring`, `injective_iff`, `Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap`, `injective_of_isSemisimpleRing`, `Flat.iff_characterModule_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_iff` 📖	mathematical	—	`Injective` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—
`injective_iff_ulift_injective` 📖	mathematical	—	`Injective` `ULift.addCommGroup` `ULift.module'` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`ulift_injective_of_injective` `injective_of_ulift_injective`
`injective_of_ulift_injective` 📖	mathematical	—	`Injective`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Injective.out` `LinearEquiv.injective`
`ulift_injective_of_injective` 📖	mathematical	—	`Injective` `ULift.addCommGroup` `ULift.module'` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Baer.injective` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Baer.iff_injective` `ULift.ext`

Module.Baer

Definitions

Name	Category	Theorems
`ExtensionOf` 📖	CompData	2 math math: `extensionOfMax_le`, `ExtensionOf.toLinearPMap_injective`
`extensionOfMax` 📖	CompOp	3 math math: `extensionOfMax_le`, `extensionOfMax_to_submodule_eq_top`, `ExtensionOfMaxAdjoin.eqn`
`extensionOfMaxAdjoin` 📖	CompOp	1 math math: `extensionOfMax_le`
`instMinExtensionOf` 📖	CompOp	—
`instPartialOrderExtensionOf` 📖	CompOp	1 math math: `extensionOfMax_le`
`instSemilatticeInfExtensionOf` 📖	CompOp	—
`supExtensionOfMaxSingleton` 📖	CompOp	1 math math: `ExtensionOfMaxAdjoin.eqn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chain_linearPMap_of_chain_extensionOf` 📖	mathematical	`IsChain` `ExtensionOf` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderExtensionOf`	`LinearPMap` `LinearPMap.le` `Set.image` `ExtensionOf.toLinearPMap`	—	—
`extensionOfMax_is_max` 📖	—	`ExtensionOf` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderExtensionOf` `extensionOfMax`	—	—	`IsMax.eq_of_ge` `zorn_le_nonempty` `ExtensionOf.le_max`
`extensionOfMax_le` 📖	mathematical	`Module.Baer`	`ExtensionOf` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderExtensionOf` `extensionOfMax` `extensionOfMaxAdjoin`	—	`le_sup_left` `ExtensionOfMaxAdjoin.extensionToFun_wd` `zero_smul` `add_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`extensionOfMax_to_submodule_eq_top` 📖	mathematical	`Module.Baer`	`LinearPMap.domain` `ExtensionOf.toLinearPMap` `extensionOfMax` `Top.top` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	`Submodule.eq_top_iff'` `extensionOfMax_is_max` `extensionOfMax_le` `extensionOfMaxAdjoin.eq_1` `Submodule.mem_sup` `Submodule.zero_mem` `Submodule.mem_span_singleton_self` `zero_add`
`extension_property` 📖	mathematical	`Module.Baer` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`LinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `extensionOfMax_to_submodule_eq_top` `LinearPMap.map_add` `IsScalarTower.left` `LinearPMap.map_smul` `LinearMap.ext` `ExtensionOf.le` `ExtensionOf.is_extension`
`extension_property_addMonoidHom` 📖	mathematical	`Module.Baer` `Int.instRing` `AddCommGroup.toIntModule` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike`	`AddMonoidHom.comp`	—	`RingHomCompTriple.ids` `extension_property` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`iff_injective` 📖	mathematical	—	`Module.Baer` `Module.Injective`	—	`injective` `of_injective`
`injective` 📖	mathematical	`Module.Baer`	`Module.Injective`	—	`RingHomCompTriple.ids` `extension_property` `DFunLike.congr_fun`
`of_equiv` 📖	—	`Module.Baer`	—	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`of_injective` 📖	mathematical	—	`Module.Baer`	—	`RingHomInvPair.ids` `small_subtype` `RingHomCompTriple.ids` `Module.Injective.out` `LinearEquiv.injective` `Subtype.val_injective` `Equiv.symm_apply_apply`

Module.Baer.ExtensionOf

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`max` 📖	CompOp	1 math math: `le_max`
`toLinearPMap` 📖	CompOp	7 math math: `Module.Baer.chain_linearPMap_of_chain_extensionOf`, `is_extension`, `dExt_iff`, `Module.Baer.extensionOfMax_to_submodule_eq_top`, `le`, `Module.Baer.ExtensionOfMaxAdjoin.eqn`, `toLinearPMap_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dExt` 📖	—	`LinearPMap.domain` `toLinearPMap` `LinearPMap.toFun'`	—	—	`ext`
`dExt_iff` 📖	mathematical	—	`LinearPMap.toFun'` `toLinearPMap`	—	`dExt`
`ext` 📖	—	`LinearPMap.domain` `toLinearPMap` `LinearPMap.toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	—	—	`RingHomSurjective.ids` `LinearPMap.ext`
`is_extension` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `LinearPMap.toFun'` `toLinearPMap` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `le`	—	—
`le` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.domain` `toLinearPMap`	—	—
`le_max` 📖	mathematical	`IsChain` `Module.Baer.ExtensionOf` `Preorder.toLE` `PartialOrder.toPreorder` `Module.Baer.instPartialOrderExtensionOf` `Set.Nonempty` `Set` `Set.instMembership`	`max`	—	`LinearPMap.le_sSup` `IsChain.directedOn` `instReflLe` `Module.Baer.chain_linearPMap_of_chain_extensionOf` `Set.mem_image`
`toLinearPMap_injective` 📖	mathematical	—	`Module.Baer.ExtensionOf` `LinearPMap` `toLinearPMap`	—	`ext` `Submodule.ext`

Module.Baer.ExtensionOfMaxAdjoin

Definitions

Name	Category	Theorems
`extendIdealTo` 📖	CompOp	5 math math: `extensionToFun_wd`, `extendIdealTo_wd`, `extendIdealTo_eq`, `extendIdealTo_is_extension`, `extendIdealTo_wd'`
`extensionToFun` 📖	CompOp	1 math math: `extensionToFun_wd`
`fst` 📖	CompOp	1 math math: `eqn`
`ideal` 📖	CompOp	—
`idealTo` 📖	CompOp	1 math math: `extendIdealTo_is_extension`
`snd` 📖	CompOp	1 math math: `eqn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqn` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Module.Baer.supExtensionOfMaxSingleton` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearPMap.domain` `Module.Baer.ExtensionOf.toLinearPMap` `Module.Baer.extensionOfMax` `fst` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `snd`	—	—
`extendIdealTo_eq` 📖	mathematical	`Module.Baer` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Module.Baer.ExtensionOf.toLinearPMap` `Module.Baer.extensionOfMax` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `LinearMap.instFunLike` `extendIdealTo` `LinearPMap.toFun'`	—	`extendIdealTo_is_extension`
`extendIdealTo_is_extension` 📖	mathematical	`Module.Baer` `Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ideal`	`DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `extendIdealTo` `Submodule.addCommMonoid` `Submodule.module` `idealTo`	—	—
`extendIdealTo_wd` 📖	mathematical	`Module.Baer` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `LinearMap.instFunLike` `extendIdealTo`	—	`sub_eq_zero` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `extendIdealTo_wd'` `sub_smul`
`extendIdealTo_wd'` 📖	mathematical	`Module.Baer` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `LinearMap.instFunLike` `extendIdealTo`	—	`Submodule.zero_mem` `extendIdealTo_is_extension` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `LinearPMap.map_zero`
`extensionToFun_wd` 📖	mathematical	`Module.Baer` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Module.Baer.supExtensionOfMaxSingleton` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearPMap.domain` `Module.Baer.ExtensionOf.toLinearPMap` `Module.Baer.extensionOfMax` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`extensionToFun` `LinearPMap.toFun'` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `LinearMap.instFunLike` `extendIdealTo`	—	`sub_smul` `sub_eq_zero` `sub_sub_sub_eq` `eqn` `Submodule.sub_mem` `extendIdealTo_eq` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_assoc` `LinearPMap.map_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `add_sub` `eq_sub_of_add_eq`

Module.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extension_property` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`LinearMap.comp` `RingHomCompTriple.ids`	—	`Module.Baer.extension_property` `Module.Baer.of_injective`
`out` 📖	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	—
`pi` 📖	mathematical	`Module.Injective`	`Pi.addCommGroup` `Pi.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomCompTriple.ids` `DFunLike.congr_fun` `extension_property`

---

← Back to Index