Theorems · Theorem · ring theory
LinearMap.ext_ring
∀ {R : Type u_1} {S : Type u_5} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₃]
[inst_3 : Module S M₃] {σ : R →+* S} {f g : R →ₛₗ[σ] M₃}, f 1 = g 1 → f = gIf two σ-linear maps from R are equal on 1, then they are equal.
- Defined in
- Mathlib.Algebra.Module.LinearMap.Defs
- Cited by
- 152 results in Mathlib
- Foundations
- Depth 23 from the axioms, rests on 175 definitions · uses 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.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapstatement and proof · cited by 10,215
- RingHomstatement and proof · cited by 10,189
- mul_oneproof · cited by 3,885
- LinearMap.extproof · cited by 844
- smul_eq_mulproof · cited by 357
- LinearMap.map_smulₛₗproof · cited by 17
Cited by152
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.ext_ringproof · cited by 16
- Module.FinitePresentation.fg_kerproof · cited by 6
- IsBaseChange.of_lift_uniqueproof · cited by 5
- Module.Relations.Quotient.linearMap_extproof · cited by 5
- Finsupp.linearCombination_linear_compproof · cited by 4
- Polynomial.taylor_coeffproof · cited by 4
- Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChangeproof · cited by 4
- LieModule.toEnd_baseChangeproof · cited by 3
- DFinsupp.linearIndependent_singleproof · cited by 3
- IsLocalizedModule.map_linearCombinationproof · cited by 3
- Module.FinitePresentation.exists_lift_of_isLocalizedModuleproof · cited by 3
- LinearMap.baseChange_idproof · cited by 3