Pi

📁 Source: Mathlib/Data/Int/Cast/Pi.lean

Statistics

Metric	Count
Definitions instIntCast	1
Theorems intCast_apply, intCast_def, elim_intCast_intCast	3
Total	4

Pi

Definitions

Name	Category	Theorems
instIntCast 📖	CompOp	31 math math: hasStrictDerivAt_intCast, fderiv_intCast, ContinuousMap.coe_intCast, differentiable_intCast, fderivWithin_intCast, hasFDerivWithinAt_intCast, BoundedContinuousFunction.coe_intCast, Function.mulSupport_intCast, Function.support_intCast, MeromorphicOn.divisor_intCast, intCast_def, measurable_intCast, derivWithin_intCast, hasDerivAtFilter_intCast, hasDerivAt_intCast, lp.infty_coeFn_intCast, intCast_memℓp_infty, differentiableAt_intCast, hasFDerivAt_intCast, ModularForm.coe_intCast, deriv_intCast, differentiableOn_intCast, meromorphicOrderAt_const_intCast, hasDerivWithinAt_intCast, Sum.elim_intCast_intCast, hasStrictFDerivAt_intCast, Matrix.diagonal_intCast', differentiableWithinAt_intCast, intCast_apply, SlashInvariantForm.coe_intCast, hasFDerivAtFilter_intCast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intCast_apply 📖	mathematical	—	instIntCast	—	—
intCast_def 📖	mathematical	—	instIntCast	—	—

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim_intCast_intCast 📖	mathematical	—	Pi.instIntCast	—	—

---

← Back to Index