Documentation Verification Report

GaussNorm

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

Statistics

Metric	Count
Definitions `gaussNorm`	1
Theorems `exists_eq_gaussNorm`, `exists_min_eq_gaussNorm`, `gaussNorm_C`, `gaussNorm_coe_powerSeries`, `gaussNorm_eq_zero_iff`, `gaussNorm_isAbsoluteValue`, `gaussNorm_monomial`, `gaussNorm_mul`, `gaussNorm_mul_le`, `gaussNorm_nonneg`, `gaussNorm_zero`, `gaussNorm_zero_right`, `isNonarchimedean_gaussNorm`, `le_gaussNorm`, `gaussNorm_C`, `gaussNorm_monomial`	16
Total	17

Polynomial

Definitions

Name	Category	Theorems
`gaussNorm` 📖	CompOp	18 math math: `isNonarchimedean_gaussNorm`, `exists_min_eq_gaussNorm`, `le_gaussNorm`, `gaussNorm_eq_zero_iff`, `exists_eq_gaussNorm`, `gaussNorm_mul`, `gaussNorm_zero`, `gaussNorm_isAbsoluteValue`, `contentIdeal_eq_top_iff_forall_gaussNorm_eq_one`, `gaussNorm_intAdicAbv_le_one`, `gaussNorm_lt_one_iff_contentIdeal_le`, `gaussNorm_monomial`, `gaussNorm_zero_right`, `gaussNorm_C`, `gaussNorm_coe_powerSeries`, `gaussNorm_nonneg`, `gaussNorm_mul_le`, `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.toPow` `Real.instMonoid`	—	`Finset.exists_mem_eq_sup'` `gaussNorm_zero` `map_zero` `MulZeroClass.zero_mul`
`exists_min_eq_gaussNorm` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`gaussNorm` `Real` `Real.instMul` `DFunLike.coe` `coeff` `Monoid.toPow` `Real.instMonoid` `Real.instLT`	—	`exists_eq_gaussNorm` `Set.mem_setOf` `Nat.find_spec` `lt_of_le_of_ne` `le_gaussNorm`
`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` `Real` `Real.instZero` `Polynomial` `instZero`	—	`gaussNorm_coe_powerSeries` `le_of_lt` `PowerSeries.gaussNorm_eq_zero_iff` `coeff_coe` `coe_eq_zero_iff`
`gaussNorm_isAbsoluteValue` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instLT` `Real.instZero`	`IsAbsoluteValue` `Real` `Real.semiring` `Real.partialOrder` `Polynomial` `Ring.toSemiring` `semiring` `gaussNorm` `AbsoluteValue` `AbsoluteValue.funLike`	—	`gaussNorm_nonneg` `AbsoluteValue.nonnegHomClass` `le_of_lt` `gaussNorm_eq_zero_iff` `AbsoluteValue.zeroHomClass` `AbsoluteValue.eq_zero` `gaussNorm_mul`
`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.toPow` `Real.instMonoid`	—	`monomial_zero_right` `map_zero` `MulZeroClass.zero_mul` `support_monomial` `Finset.sup'_congr` `coeff_monomial_same`
`gaussNorm_mul` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `AbsoluteValue` `Ring.toSemiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instLT` `Real.instZero`	`gaussNorm` `AbsoluteValue` `Real` `Ring.toSemiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Polynomial` `instMul` `Real.instMul`	—	`le_antisymm` `gaussNorm_mul_le` `AbsoluteValue.zeroHomClass` `AbsoluteValue.nonnegHomClass` `AbsoluteValue.mulHomClass` `le_of_lt`
`gaussNorm_mul_le` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `Real.instLE` `Real.instZero`	`Real` `Real.instLE` `gaussNorm` `Polynomial` `instMul` `Real.instMul`	—	`eq_or_ne` `gaussNorm_zero` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `support_nonempty` `left_ne_zero_of_mul` `right_ne_zero_of_mul` `Finset.sup'_congr` `coeff_mul` `Finset.sum_congr` `IsNonarchimedean.finset_image_add_of_nonempty` `Finset.nonempty_range_add_one` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Nat.instNoMaxOrder` `le_gaussNorm` `gaussNorm_nonneg` `mul_le_mul` `mul_nonneg` `NonnegHomClass.apply_nonneg`
`gaussNorm_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Real` `Real.instLE` `Real.instZero` `gaussNorm`	—	`instReflLe`
`gaussNorm_zero` 📖	mathematical	—	`gaussNorm` `Polynomial` `instZero` `Real` `Real.instZero`	—	—
`gaussNorm_zero_right` 📖	mathematical	—	`gaussNorm` `Real` `Real.instZero` `DFunLike.coe` `coeff`	—	`zero_pow` `MulZeroClass.mul_zero` `pow_zero` `mul_one` `eq_or_ne` `Finset.sup'.congr_simp` `map_zero` `Finset.sup'_const` `le_antisymm` `instReflLe`
`isNonarchimedean_gaussNorm` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `Real.instLE` `Real.instZero`	`IsNonarchimedean` `Real` `Real.linearOrder` `Polynomial` `instAdd` `gaussNorm`	—	`eq_or_ne` `zero_add` `gaussNorm_zero` `add_zero` `coeff_add` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `max_mul_of_nonneg` `Real.instZeroLEOneClass` `max_le_max` `le_gaussNorm`
`le_gaussNorm` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Real` `Real.instLE` `Real.instMul` `DFunLike.coe` `coeff` `Monoid.toPow` `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` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `C` `Real`	—	`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` `MvPowerSeries.instAddCommMonoid` `Semiring.toModule` `MvPowerSeries.instModule` `LinearMap.instFunLike` `monomial` `Real` `Real.instMul` `Monoid.toPow` `Real.instMonoid`	—	`Polynomial.gaussNorm_coe_powerSeries` `Polynomial.gaussNorm_monomial`

---

← Back to Index