Theorems · Theorem · linear algebra
LinearMap.restrictScalars.congr_simp
∀ (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ₗ fₗ_1 : M →ₗ[S] M₂),
fₗ = fₗ_1 → ↑R fₗ = ↑R fₗ_1- Cited by
- 5 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.
Cites7
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.restrictScalarsstatement and proof · cited by 215
- LinearMap.CompatibleSMulstatement and proof · cited by 86
Cited by5
Results whose statement or proof uses this declaration.
- IsLocalRing.map_tensorProduct_mk_eq_topproof · cited by 4
- Module.injective_of_isLocalizedModuleproof · cited by 2
- Algebra.Generators.liftBaseChange_injective_of_isLocalizationAwayproof · cited by 2
- Module.injective_of_localization_maximalproof · cited by 2
- TensorProduct.restrictScalar_directSumRightproof · cited by 2