Documentation Verification Report

Norm

📁 Source: Mathlib/Analysis/Polynomial/Norm.lean

Statistics

Metric	Count
Definitions `supNorm`	1
Theorems `exists_eq_supNorm`, `isGreatest_supNorm`, `le_supNorm`, `supNorm_C`, `supNorm_X`, `supNorm_def'`, `supNorm_eq_iSup`, `supNorm_eq_zero_iff`, `supNorm_monomial`, `supNorm_nonneg`, `supNorm_zero`	11
Total	12

Polynomial

Definitions

Name	Category	Theorems
`supNorm` 📖	CompOp	12 math math: `exists_eq_supNorm`, `supNorm_zero`, `supNorm_X`, `le_supNorm`, `supNorm_nonneg`, `supNorm_monomial`, `supNorm_C`, `supNorm_def'`, `supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure`, `isGreatest_supNorm`, `supNorm_eq_iSup`, `supNorm_eq_zero_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_supNorm` 📖	mathematical	—	`supNorm` `Norm.norm` `SeminormedRing.toNorm` `coeff` `Ring.toSemiring` `SeminormedRing.toRing`	—	`one_pow` `mul_one` `exists_eq_gaussNorm` `AddGroupSeminormClass.toZeroHomClass` `RingSeminormClass.toAddGroupSeminormClass` `RingSeminorm.ringSeminormClass`
`isGreatest_supNorm` 📖	mathematical	—	`IsGreatest` `Real` `Real.instLE` `Set.range` `Norm.norm` `SeminormedRing.toNorm` `coeff` `Ring.toSemiring` `SeminormedRing.toRing` `supNorm`	—	`exists_eq_supNorm` `le_supNorm`
`le_supNorm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `SeminormedRing.toNorm` `coeff` `Ring.toSemiring` `SeminormedRing.toRing` `supNorm`	—	`one_pow` `mul_one` `le_gaussNorm` `AddGroupSeminormClass.toZeroHomClass` `RingSeminormClass.toAddGroupSeminormClass` `RingSeminorm.ringSeminormClass` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isNat_le_true` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one`
`supNorm_C` 📖	mathematical	—	`supNorm` `DFunLike.coe` `RingHom` `Polynomial` `Ring.toSemiring` `SeminormedRing.toRing` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Norm.norm` `SeminormedRing.toNorm`	—	`gaussNorm_C` `AddGroupSeminormClass.toZeroHomClass` `RingSeminormClass.toAddGroupSeminormClass` `RingSeminorm.ringSeminormClass`
`supNorm_X` 📖	mathematical	—	`supNorm` `X` `Ring.toSemiring` `SeminormedRing.toRing` `Real` `Real.instOne`	—	`monomial_one_one_eq_X` `supNorm_monomial` `NormOneClass.norm_one`
`supNorm_def'` 📖	mathematical	—	`supNorm` `Real` `Finset.Nonempty` `support` `Ring.toSemiring` `SeminormedRing.toRing` `Finset.decidableNonempty` `Finset.sup'` `Real.instSemilatticeSup` `Norm.norm` `SeminormedRing.toNorm` `coeff` `Real.instZero`	—	`Finset.sup'_congr` `one_pow` `mul_one`
`supNorm_eq_iSup` 📖	mathematical	—	`supNorm` `iSup` `Real` `Real.instSupSet` `Norm.norm` `SeminormedRing.toNorm` `coeff` `Ring.toSemiring` `SeminormedRing.toRing`	—	`IsGreatest.csSup_eq` `isGreatest_supNorm`
`supNorm_eq_zero_iff` 📖	mathematical	—	`supNorm` `NormedRing.toSeminormedRing` `Real` `Real.instZero` `Polynomial` `Ring.toSemiring` `NormedRing.toRing` `instZero`	—	`gaussNorm_eq_zero_iff` `AddGroupSeminormClass.toZeroHomClass` `RingSeminormClass.toAddGroupSeminormClass` `RingSeminorm.ringSeminormClass` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`supNorm_monomial` 📖	mathematical	—	`supNorm` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `SeminormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Norm.norm` `SeminormedRing.toNorm`	—	`monomial_zero_right` `supNorm_zero` `norm_zero` `support_monomial` `Finset.sup'_congr` `one_pow` `mul_one` `coeff_monomial_same`
`supNorm_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `supNorm`	—	`gaussNorm_nonneg` `Mathlib.Meta.NormNum.isNat_le_true` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `RingSeminorm.ringSeminormClass`
`supNorm_zero` 📖	mathematical	—	`supNorm` `Polynomial` `Ring.toSemiring` `SeminormedRing.toRing` `instZero` `Real` `Real.instZero`	—	`gaussNorm_zero`

---

← Back to Index