Theorems · Theorem · functional analysis
ContinuousLinearMap.map_zero
∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
[inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
[inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂), f 0 = 0- Cited by
- 17 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext
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
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- RingHomstatement and proof · cited by 10,189
- ContinuousLinearMapstatement and proof · cited by 5,352
- map_zeroproof · cited by 1,614
Cited by17
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.map_zero₂proof · cited by 5
- HasCompactSupport.convolutionExists_rightproof · cited by 4
- HasFDerivAt.comp_semilinearproof · cited by 3
- ContinuousLinearMap.exists_preimage_norm_leproof · cited by 2
- BoxIntegral.hasIntegral_zeroproof · cited by 2
- Real.one_div_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 2
- MeasureTheory.convolution_integrand_bound_right_of_le_of_subsetproof · cited by 2
- MeasureTheory.support_convolution_subset_swapproof · cited by 2
- ContinuousLinearMap.integral_comp_comm'proof · cited by 2
- ContinuousLinearMap.integral_comp_commSLproof · cited by 2
- Real.one_add_rpow_hasFPowerSeriesOnBall_zeroproof · cited by 1
- ContinuousLinearEquiv.map_zeroproof · cited by 1