Theorems · Theorem · ring theory
LinearMap.restrictScalars_injective
∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
[inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S], Function.Injective ↑R- Defined in
- Mathlib.Algebra.Module.LinearMap.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapstatement and proof · cited by 10,215
- LinearMap.extproof · cited by 844
- LinearMap.restrictScalarsstatement and proof · cited by 215
- LinearMap.congr_funproof · cited by 96
- LinearMap.CompatibleSMulstatement and proof · cited by 86
Cited by11
Results whose statement or proof uses this declaration.
- TensorProduct.AlgebraTensorModule.curry_injectiveproof · cited by 159
- exists_bijective_map_powersproof · cited by 3
- Module.injective_of_isLocalizedModuleproof · cited by 2
- Module.injective_of_localization_maximalproof · cited by 2
- IsSimpleModule.algebraMap_end_bijective_of_isAlgClosedproof · cited by 2
- Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRingproof · cited by 1
- IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐproof · cited by 1
- LinearMap.restrictScalars_injproof · cited by 1
- LinearMap.split_surjective_of_localization_maximalproof · cited by 1
- Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijectiveproof · cited by 1
- KaehlerDifferential.tensorKaehlerEquiv_left_invproof · cited by 0