Theorem Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'

Modification history

2023-05-11 14:58

Mathlib/Algebra/Module/Injective.lean

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

Added Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'View on Github →