Theorems · Definition · ring theory
Module.Baer
(R : Type u) → [inst : Ring R] → (Q : Type v) → [inst_1 : AddCommGroup Q] → [Module R Q] → Prop
An R-module Q satisfies Baer's criterion if any R-linear map from an Ideal R extends to
an R-linear map R ⟶ Q
- Defined in
- Mathlib.Algebra.Module.Injective
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idproof · cited by 18,349
- AddCommGroupstatement and proof · cited by 12,871
- LinearMapproof · cited by 10,215
- Ringstatement and proof · cited by 7,463
- Idealproof · cited by 4,748
Cited by23
Results whose statement or proof uses this declaration.
- Module.Baer.ExtensionOfMaxAdjoin.extendIdealTostatement and proof · cited by 7
- Module.Baer.of_injectivestatement · cited by 5
- Module.Baer.iff_injectivestatement · cited by 4
- Module.Baer.injectivestatement and proof · cited by 4
- Module.Baer.extension_propertystatement and proof · cited by 3
- Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extensionstatement and proof · cited by 2
- Module.injective_of_isLocalizedModuleproof · cited by 2
- Module.injective_of_localization_maximalproof · cited by 2
- Module.Baer.extensionOfMaxAdjoinstatement and proof · cited by 2
- Module.Baer.of_equivstatement and proof · cited by 2
- Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eqstatement and proof · cited by 1
- Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd'statement and proof · cited by 1