Theorems · Theorem · commutative algebra
LinearEquiv.restrictScalars_toLinearMap
∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [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₂),
↑(LinearEquiv.restrictScalars R f) = ↑R ↑f- Defined in
- Mathlib.Algebra.Module.Equiv.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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 · cited by 10,215
- LinearEquivstatement and proof · cited by 3,317
- LinearEquiv.toLinearMapstatement and proof · cited by 1,171
- LinearMap.restrictScalarsstatement · cited by 215
- LinearMap.CompatibleSMulstatement and proof · cited by 86
- LinearEquiv.restrictScalarsstatement and proof · cited by 46
Cited by10
Results whose statement or proof uses this declaration.
- Ideal.comap_map_eq_self_of_faithfullyFlatproof · cited by 4
- Module.injective_of_localization_maximalproof · cited by 2
- TensorProduct.restrictScalar_directSumRightproof · cited by 2
- IsBaseChange.iff_of_equiv_commproof · cited by 1
- Algebra.TensorProduct.distribBaseChange_comp_includeLeftSubRightproof · cited by 1
- LinearMap.localizedMap_surjective_iff_subsingleton_localized_cokerproof · cited by 1
- Algebra.Extension.tensorToH1Cotangent_bijective_of_flatproof · cited by 0
- IsBaseChange.comp_equivproof · cited by 0
- RootPairing.coroot_mem_or_neg_mem_closure_of_rootproof · cited by 0
- Module.Flat.toAlgebra_injectiveproof · cited by 0