Theorems · Theorem · functional analysis

ContinuousLinearMap.intCast_apply

Deprecated since 2026-05-20Use intCast_apply instead.

∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : IntCast F} {inst_2 : SMul ℤ α}
  [self : IsIntCastApply F α] (n : ℤ) (x : α), ↑n x = n • x

Alias of intCast_apply.

Defined in: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms
Assumes: IsIntCastApply

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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

DFunLike.coestatement · cited by 62,936
FunLikestatement · cited by 2,560
IsIntCastApplystatement · cited by 5
intCast_applyproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.