Mathlib Map

Theorems · Theorem · operator theory

IsCompactOperator.smul_unit_iff

∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {S : Type u_6} [inst_4 : Monoid S]
  [inst_5 : DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂} {c : Sˣ},
  IsCompactOperator (c • f) ↔ IsCompactOperator f
Defined in
Mathlib.Analysis.Normed.Operator.Compact.Basic
Cited by
1 results in Mathlib
Foundations
Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceAddCommMonoidTopologicalSpaceAddCommMonoidMonoidDistribMulActionContinuousConstSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsCompactOperator.smul_isUnit_iff · cited by 2IsCompactOperator.smul_is…TopologicalSpace · cited by 24529TopologicalSpaceAddCommMonoid · cited by 12281AddCommMonoidMonoid · cited by 3887MonoidUnits · cited by 2804UnitsContinuousConstSMul · cited by 832ContinuousConstSMulDistribMulAction · cited by 584DistribMulActioninv_smul_smul · cited by 76inv_smul_smulIsCompactOperator · cited by 51IsCompactOperatorIsCompactOperator.smul · cited by 1IsCompactOperator.smulIsCompactOperator.smul_unit_i…CITED BYCITES

Cites9

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.