Commit 2023-05-11 14:58 791d8ddd

View on Github →

feat: port Algebra.Module.Injective (#3873)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Injective.lean

added theorem Module.Baer.ExtensionOf.ext

added theorem Module.Baer.ExtensionOf.ext_iff

added theorem Module.Baer.ExtensionOf.le_max

added def Module.Baer.ExtensionOf.max

added structure Module.Baer.ExtensionOf

added theorem Module.Baer.ExtensionOfMaxAdjoin.eqn

added def Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo

added theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq

added theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension

added theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'

added theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd

added def Module.Baer.ExtensionOfMaxAdjoin.extensionToFun

added theorem Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd

added def Module.Baer.ExtensionOfMaxAdjoin.fst

added def Module.Baer.ExtensionOfMaxAdjoin.ideal

added def Module.Baer.ExtensionOfMaxAdjoin.idealTo

added def Module.Baer.ExtensionOfMaxAdjoin.snd

added theorem Module.Baer.chain_linearPMap_of_chain_extensionOf

added def Module.Baer.extensionOfMax

added def Module.Baer.extensionOfMaxAdjoin

added theorem Module.Baer.extensionOfMax_is_max

added theorem Module.Baer.extensionOfMax_le

added theorem Module.Baer.extensionOfMax_to_submodule_eq_top

added def Module.Baer.supExtensionOfMaxSingleton

added def Module.Baer

added theorem Module.injective_iff_injective_object

added theorem Module.injective_module_of_injective_object

added theorem Module.injective_object_of_injective_module