Theorems · Theorem · ring theory
LinearMap.coe_restrictScalars
∀ (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] (f : M →ₗ[S] M₂),
⇑(↑R f) = ⇑f- Defined in
- Mathlib.Algebra.Module.LinearMap.Defs
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- 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.restrictScalarsstatement · cited by 215
- LinearMap.CompatibleSMulstatement and proof · cited by 86
Cited by14
Results whose statement or proof uses this declaration.
- LocalizedModule.coe_map_eqproof · cited by 4
- span_eq_top_of_isLocalizedModuleproof · cited by 3
- isConformalMap_complex_linearproof · cited by 3
- Module.injective_of_localization_maximalproof · cited by 2
- LinearMap.polyCharpolyAux_baseChangeproof · cited by 2
- Module.nonempty_basis_of_flat_of_finrank_eqproof · cited by 1
- dvd_differentIdeal_of_not_isSeparableproof · cited by 1
- IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐproof · cited by 1
- pow_sub_one_dvd_differentIdeal_auxproof · cited by 1
- LinearMap.IsSymmetric.restrictScalarsproof · cited by 1
- Module.Basis.ofIsLocalizedModule_repr_applyproof · cited by 1
- Algebra.tensorH1CotangentOfIsLocalization_toLinearMapproof · cited by 0