Bounds

Statistics

Metric	Count
Definitions	0
Theorems `norm_le_one`, `unit_norm_eq_one`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_le_one` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `Real.instOne`	—	`Eq.le` `unit_norm_eq_one` `MulChar.map_nonunit` `norm_zero` `zero_le_one` `Real.instZeroLEOneClass`
`unit_norm_eq_one` 📖	mathematical	—	`Norm.norm` `NormedField.toNorm` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real` `Real.instOne`	—	`pow_eq_one_iff_of_nonneg` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `norm_nonneg` `LT.lt.ne'` `Nat.card_pos` `instFiniteZModUnits` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `map_pow` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `Units.val_pow_eq_pow_val` `pow_card_eq_one'` `Units.val_one` `map_one` `MonoidHomClass.toOneHomClass` `NormOneClass.norm_one`

---