Mathlib Changelog
v4
Changelog
About
Github
Theorem
Metric.unitSphere.coe_pow
Modification history
2025-04-19 07:26
Mathlib/Analysis/Normed/Field/UnitBall.lean
chore(Normed/Field/UnitBall): review instances (#24188)
Added
Metric.unitSphere.coe_pow
View on Github →