Documentation Verification Report

Restricted

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

Statistics

Metric	Count
Definitions `IsRestricted`, `convergenceSet`	2
Theorems `C`, `add`, `convergenceSet_BddAbove`, `isRestricted_iff`, `isRestricted_iff_abs`, `monomial`, `mul`, `neg`, `one`, `smul`, `zero`	11
Total	13

PowerSeries

Definitions

Name	Category	Theorems
`IsRestricted` 📖	MathDef	6 math math: `IsRestricted.isRestricted_iff`, `IsRestricted.one`, `IsRestricted.monomial`, `IsRestricted.C`, `IsRestricted.zero`, `IsRestricted.isRestricted_iff_abs`

PowerSeries.IsRestricted

Definitions

Name	Category	Theorems
`convergenceSet` 📖	CompOp	1 math math: `convergenceSet_BddAbove`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C` 📖	mathematical	—	`PowerSeries.IsRestricted` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `NormedRing.toRing` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.C`	—	`PowerSeries.monomial_zero_eq_C_apply` `monomial`
`add` 📖	mathematical	`PowerSeries.IsRestricted`	`PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PowerSeries.instRing` `NormedRing.toRing`	—	`map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `abs_norm` `le_imp_le_of_le_of_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `norm_add_le` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_refl` `add_mul` `Distrib.rightDistribClass` `add_lt_add_of_lt_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add`
`convergenceSet_BddAbove` 📖	mathematical	`PowerSeries.IsRestricted`	`BddAbove` `Real` `Real.instLE` `convergenceSet`	—	`Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `norm_pow` `NormedDivisionRing.to_normOneClass` `bddAbove_def` `convergenceSet.eq_1` `le_total` `Finset.le_max'` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_abs_self` `norm_nonneg` `abs_pow` `LT.lt.le`
`isRestricted_iff` 📖	mathematical	—	`PowerSeries.IsRestricted` `Real` `Real.instLT` `Norm.norm` `Real.norm` `Real.instMul` `NormedRing.toNorm` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `Monoid.toNatPow` `Real.instMonoid`	—	`instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `sub_zero` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `norm_pow` `NormedDivisionRing.to_normOneClass`
`isRestricted_iff_abs` 📖	mathematical	—	`PowerSeries.IsRestricted` `abs` `Real` `Real.lattice` `Real.instAddGroup`	—	`norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `norm_pow` `NormedDivisionRing.to_normOneClass` `abs_abs` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`monomial` 📖	mathematical	—	`PowerSeries.IsRestricted` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instAddCommMonoid` `Semiring.toModule` `PowerSeries.instModule` `LinearMap.instFunLike` `PowerSeries.monomial`	—	`norm_mul` `NormedDivisionRing.toNormMulClass` `abs_norm` `norm_pow` `NormedDivisionRing.to_normOneClass` `norm_zero` `MulZeroClass.zero_mul`
`mul` 📖	mathematical	`PowerSeries.IsRestricted`	`PowerSeries` `MvPowerSeries.instMul` `Ring.toSemiring` `NormedRing.toRing`	—	`bddAbove_iff_exists_ge` `convergenceSet_BddAbove` `isRestricted_iff_abs` `PowerSeries.coeff_mul` `norm_mul` `NormedDivisionRing.toNormMulClass` `abs_norm` `norm_pow` `NormedDivisionRing.to_normOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_max_of_lt_left` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `IsUltrametricDist.exists_norm_finset_sum_le` `zero_add` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_imp_le_of_le_of_le` `norm_mul_le` `IsOrderedRing.toZeroLEOneClass` `le_refl` `pow_add` `lt_imp_lt_of_le_of_le` `mul_le_mul_of_nonneg_left` `mul_nonneg` `norm_nonneg` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `div_mul_comm` `mul_le_iff_le_one_left` `MulPosStrictMono.toMulPosReflectLE` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `le_max_right` `Mathlib.Tactic.Bound.le_max_of_le_left_or_le_right` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_lt_mul_of_pos_left` `mul_div_left_comm` `mul_le_iff_le_one_right` `le_max_left`
`neg` 📖	mathematical	`PowerSeries.IsRestricted`	`PowerSeries` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `PowerSeries.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `norm_neg` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `norm_pow` `NormedDivisionRing.to_normOneClass`
`one` 📖	mathematical	—	`PowerSeries.IsRestricted` `PowerSeries` `MvPowerSeries.instOne` `Ring.toSemiring` `NormedRing.toRing`	—	`PowerSeries.coeff_one` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `norm_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MulZeroClass.zero_mul`
`smul` 📖	mathematical	`PowerSeries.IsRestricted`	`PowerSeries` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `PowerSeries.instAddMonoid` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `PowerSeries.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `PowerSeries.instModule` `Semiring.toModule`	—	`zero_smul` `zero` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `abs_norm` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `mul_le_mul_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `norm_mul_le` `Real.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_assoc` `mul_div_cancel₀`
`zero` 📖	mathematical	—	`PowerSeries.IsRestricted` `PowerSeries` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `norm_zero` `MulZeroClass.zero_mul` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`

---

← Back to Index