Injective

📁 Source: Mathlib/RingTheory/LocalProperties/Injective.lean

Statistics

Metric	Count
Definitions	0
Theorems injective_of_isLocalizedModule, injective_of_localization_maximal, injective_of_localization_maximal'	3
Total	3

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_of_isLocalizedModule 📖	mathematical	—	Injective CommRing.toRing	—	Baer.of_injective smulCommClass_self IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization RingHom.instRingHomClass Ideal.localized'_eq_map IsLocalization.map_comap finitePresentation_of_finite instFiniteSubtypeMemIdealOfIsNoetherian IsScalarTower.to_smulCommClass' Submodule.isLocalizedModule Submodule.isScalarTower' IsLocalizedModule.surj FinitePresentation.isLocalizedModule_mapExtendScalars LinearMap.instSMulCommClass LinearMap.instIsScalarTower IsScalarTower.left End.isUnit_iff IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass IsLocalization.map_units map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass algebraMap_smul IsLocalization.mk'_spec' LinearMap.restrictScalars_injective LinearMap.IsScalarTower.compatibleSMul IsLocalizedModule.linearMap_ext LinearMap.ext RingHomCompTriple.ids LinearMap.comp.congr_simp LinearMap.restrictScalars.congr_simp map_one MonoidHomClass.toOneHomClass one_smul IsLocalizedModule.map_apply
injective_of_localization_maximal 📖	mathematical	Injective Localization.AtPrime CommRing.toCommSemiring Ideal.IsMaximal.isPrime' OreLocalization.instRing CommRing.toRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid LocalizedModule AddCommGroup.toAddCommMonoid OreLocalization.instAddCommGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction OreLocalization.instModule	Injective CommRing.toRing	—	Ideal.IsMaximal.isPrime' Baer.iff_injective smulCommClass_self Baer.iff_surjective finitePresentation_of_finite instFiniteSubtypeMemIdealOfIsNoetherian surjective_of_localized_maximal IsScalarTower.left IsScalarTower.right Localization.isLocalization instIsLocalizedModuleLinearMapOfIsLocalization IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 Submodule.isLocalizedModule localizedModuleIsLocalizedModule Submodule.isScalarTower' LinearMap.IsScalarTower.compatibleSMul IsLocalizedModule.ext IsLocalizedModule.map_units LinearMap.ext RingHomCompTriple.ids IsLocalizedModule.map_apply LinearMap.instIsScalarTower FinitePresentation.isLocalizedModule_mapExtendScalars instFinitePresentation LinearMap.restrictScalars_injective LinearMap.comp.congr_simp LinearMap.restrictScalars.congr_simp Baer.of_injective UnivLE.small univLE_of_max UnivLE.self LinearMap.coe_restrictScalars RingHomInvPair.ids LocalizedModule.restrictScalars_map_eq
injective_of_localization_maximal' 📖	mathematical	Small IsLocalization.AtPrime CommRing.toCommSemiring Ideal.IsMaximal.isPrime' IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction AddCommGroup.toAddCommMonoid IsLocalizedModule Ideal.primeCompl Injective CommRing.toRing	Injective CommRing.toRing	—	Ideal.IsMaximal.isPrime' injective_of_localization_maximal Injective.of_ringEquiv Localization.isLocalization RingHomInvPair.ids IsScalarTower.left IsScalarTower.right localizedModuleIsLocalizedModule RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHomInvPair.of_ringEquiv IsLocalization.exists_mk'_eq smulCommClass_self End.isUnit_iff IsLocalizedModule.map_units SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass IsLocalization.smul_mk'_self algebraMap_smul IsLocalization.map_id_mk' OreLocalization.instIsScalarTower_1 LinearEquiv.left_inv LinearEquiv.right_inv

---

← Back to Index