Documentation Verification Report

GaussNorm

📁 Source: Mathlib/RingTheory/PowerSeries/GaussNorm.lean

Statistics

Metric	Count
Definitions `gaussNorm`	1
Theorems `gaussNorm_eq_zero_iff`, `gaussNorm_nonneg`, `gaussNorm_zero`, `le_gaussNorm`	4
Total	5

PowerSeries

Definitions

Name	Category	Theorems
`gaussNorm` 📖	CompOp	7 math math: `gaussNorm_monomial`, `gaussNorm_zero`, `gaussNorm_C`, `gaussNorm_eq_zero_iff`, `le_gaussNorm`, `Polynomial.gaussNorm_coe_powerSeries`, `gaussNorm_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gaussNorm_eq_zero_iff` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Real` `Real.instLT` `Real.instZero` `BddAbove` `Real.instLE` `Set.range` `Real.instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `Monoid.toNatPow` `Real.instMonoid`	`gaussNorm` `instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `ne_of_gt` `exists_coeff_ne_zero_iff_ne_zero` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_le_of_ne'` `NonnegHomClass.apply_nonneg` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `le_ciSup` `gaussNorm_zero`
`gaussNorm_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `gaussNorm`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NonnegHomClass.apply_nonneg` `pow_nonneg` `Real.instZeroLEOneClass` `le_of_lt` `zero_lt_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `le_ciSup` `ciSup_of_not_bddAbove` `Real.sSup_empty`
`gaussNorm_zero` 📖	mathematical	—	`gaussNorm` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Real` `Real.instZero`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `MulZeroClass.zero_mul` `ciSup_const`
`le_gaussNorm` 📖	mathematical	`BddAbove` `Real` `Real.instLE` `setOf` `Real.instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `Monoid.toNatPow` `Real.instMonoid`	`gaussNorm`	—	`le_ciSup`

---

← Back to Index