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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow Real.instMonoid	gaussNorm Real Real.instZero PowerSeries MvPowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	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 instReflLe
gaussNorm_zero 📖	mathematical	—	gaussNorm PowerSeries MvPowerSeries.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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow Real.instMonoid	Real Real.instLE Real.instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toPow Real.instMonoid gaussNorm	—	le_ciSup

---

← Back to Index