Theorems · Theorem · Lie groups
continuous_pow
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] (n : ℕ), Continuous fun a => a ^ n- Defined in
- Mathlib.Topology.Algebra.Monoid
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- TopologicalSpacestatement and proof · cited by 24,529
- Monoidstatement and proof · cited by 3,887
- Continuousstatement · cited by 2,592
- ContinuousMulstatement and proof · cited by 343
Cited by15
Results whose statement or proof uses this declaration.
- continuous_zpowproof · cited by 8
- Continuous.powproof · cited by 5
- ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_powproof · cited by 3
- Height.mulHeight_powproof · cited by 3
- continuousAt_powproof · cited by 2
- continuousOn_powproof · cited by 2
- Polynomial.continuous_eval₂proof · cited by 2
- intervalIntegral.intervalIntegrable_powproof · cited by 1
- Convex.addHaar_frontierproof · cited by 1
- Polynomial.mahlerMeasure_le_sqrt_sum_sq_norm_coeffproof · cited by 1
- MeasureTheory.AEEqFun.coeFn_powproof · cited by 0
- ProbabilityTheory.condVar_of_aestronglyMeasurableproof · cited by 0