Theorems · Theorem · ring theory
LinearMap.map_zero
∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
(f : M →ₛₗ[σ] M₃), f 0 = 0- Defined in
- Mathlib.Algebra.Module.LinearMap.Defs
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext
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.
- DFunLike.coestatement · 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
- map_zeroproof · cited by 1,614
Cited by54
Results whose statement or proof uses this declaration.
- LinearMap.toAddMonoidHomproof · cited by 101
- Finsupp.mapRange.linearMapproof · cited by 70
- Finsupp.mapRange.linearMap_applystatement · cited by 48
- Polynomial.monomial_zero_rightproof · cited by 25
- MeasureTheory.Measure.restrict_zeroproof · cited by 11
- LinearPMap.map_zeroproof · cited by 11
- LinearMap.lTensor_zeroproof · cited by 10
- LinearMap.comp_zeroproof · cited by 9
- Polynomial.derivative_zeroproof · cited by 8
- Polynomial.leadingCoeff_monomialproof · cited by 6
- Algebra.Generators.Cotangent.exactproof · cited by 6
- LinearMap.map_zero₂proof · cited by 5