Finite

📁 Source: Mathlib/Analysis/Normed/Ring/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_apply, norm_eq_one	2
Total	2

AddChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_apply 📖	mathematical	—	Norm.norm NormedRing.toNorm DFunLike.coe AddChar AddLeftCancelMonoid.toAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing instFunLike Real Real.instOne	—	IsOfFinOrder.norm_eq_one MonoidHom.isOfFinOrder isOfFinOrder_of_finite instFiniteMultiplicative

IsOfFinOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_eq_one 📖	mathematical	IsOfFinOrder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	Norm.norm NormedRing.toNorm Real Real.instOne	—	eq_one Real.instIsStrictOrderedRing norm_nonneg MonoidHom.isOfFinOrder

---

← Back to Index