Mathlib Map

Theorems · Theorem · functional analysis

ContinuousLinearMap.smulRight_id

∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁],
  (ContinuousLinearMap.id R₁ R₁).smulRight = ContinuousLinearMap.toSpanSingleton R₁
Defined in
Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Cited by
1 results in Mathlib
Foundations
Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SemiringTopologicalSpaceAddCommMonoidModuleTopologicalSpaceContinuousSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContinuousLinearMap.det_toSpanSingleton · cited by 6ContinuousLinearMap.det_t…TopologicalSpace · cited by 24529TopologicalSpaceModule · cited by 20661ModuleRingHom.id · cited by 18349RingHom.idSemiring · cited by 13802SemiringAddCommMonoid · cited by 12281AddCommMonoidContinuousLinearMap · cited by 5352ContinuousLinearMapContinuousSMul · cited by 1016ContinuousSMulContinuousLinearMap.id · cited by 233ContinuousLinearMap.idContinuousLinearMap.toSpanSingleton · cited by 133ContinuousLinearMap.toSpa…ContinuousLinearMap.smulRight · cited by 126ContinuousLinearMap.smulR…ContinuousLinearMap.smulRight…CITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.