Documentation Verification Report

GaussNorm

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

Statistics

Metric	Count
Definitions `gaussNorm`	1
Theorems `exists_eq_gaussNorm`, `gaussNorm_C`, `gaussNorm_coe_powerSeries`, `gaussNorm_eq_zero_iff`, `gaussNorm_monomial`, `gaussNorm_nonneg`, `gaussNorm_zero`, `le_gaussNorm`, `gaussNorm_C`, `gaussNorm_monomial`	10
Total	11

Polynomial

Definitions

Name	Category	Theorems
`gaussNorm` 📖	CompOp	12 math math: `le_gaussNorm`, `gaussNorm_eq_zero_iff`, `exists_eq_gaussNorm`, `gaussNorm_zero`, `contentIdeal_eq_top_iff_forall_gaussNorm_eq_one`, `gaussNorm_intAdicAbv_le_one`, `gaussNorm_lt_one_iff_contentIdeal_le`, `gaussNorm_monomial`, `gaussNorm_C`, `gaussNorm_coe_powerSeries`, `gaussNorm_nonneg`, `isPrimitive_iff_forall_gaussNorm_eq_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_gaussNorm` 📖	mathematical	—	`gaussNorm` `Real` `Real.instMul` `DFunLike.coe` `coeff` `Monoid.toNatPow` `Real.instMonoid`	—	`Finset.exists_mem_eq_sup'` `gaussNorm_zero` `map_zero` `MulZeroClass.zero_mul`
`gaussNorm_C` 📖	mathematical	—	`gaussNorm` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Real`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `support_C` `Finset.sup'_congr` `coeff_C_zero` `pow_zero` `mul_one`
`gaussNorm_coe_powerSeries` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`PowerSeries.gaussNorm` `toPowerSeries` `gaussNorm`	—	`PowerSeries.gaussNorm_zero` `gaussNorm_zero` `coeff_coe` `le_antisymm` `ciSup_le` `Finset.le_sup'` `map_zero` `MulZeroClass.zero_mul` `support_nonempty` `exists_eq_gaussNorm` `le_ciSup`
`gaussNorm_eq_zero_iff` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Real` `Real.instLT` `Real.instZero`	`gaussNorm` `Polynomial` `instZero`	—	`gaussNorm_coe_powerSeries` `le_of_lt` `PowerSeries.gaussNorm_eq_zero_iff` `coeff_coe` `coe_eq_zero_iff`
`gaussNorm_monomial` 📖	mathematical	—	`gaussNorm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`monomial_zero_right` `map_zero` `MulZeroClass.zero_mul` `support_monomial` `Finset.sup'_congr` `coeff_monomial_same`
`gaussNorm_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`gaussNorm`	—	—
`gaussNorm_zero` 📖	mathematical	—	`gaussNorm` `Polynomial` `instZero` `Real` `Real.instZero`	—	—
`le_gaussNorm` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Real.instMul` `DFunLike.coe` `coeff` `Monoid.toNatPow` `Real.instMonoid` `gaussNorm`	—	`gaussNorm_coe_powerSeries` `coeff_coe` `PowerSeries.le_gaussNorm`

PowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gaussNorm_C` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`gaussNorm` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `C`	—	`Polynomial.gaussNorm_coe_powerSeries` `Polynomial.gaussNorm_C`
`gaussNorm_monomial` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`gaussNorm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`Polynomial.gaussNorm_coe_powerSeries` `Polynomial.gaussNorm_monomial`

---

← Back to Index