Documentation Verification Report

LinearTopology

📁 Source: Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean

Statistics

Metric	Count
Definitions `basis`	1
Theorems `basis_le`, `basis_le_iff`, `hasBasis_nhds_zero`, `instIsLinearTopologyMulOpposite`, `instIsLinearTopologyOfMulOpposite`, `isTopologicallyNilpotent_iff_constantCoeff`, `isTopologicallyNilpotent_of_constantCoeff`, `mem_basis_iff`	8
Total	9

MvPowerSeries.LinearTopology

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	4 math math: `basis_le_iff`, `mem_basis_iff`, `hasBasis_nhds_zero`, `basis_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_le` 📖	mathematical	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLE`	`MvPowerSeries` `MvPowerSeries.instRing` `basis`	—	`le_trans`
`basis_le_iff` 📖	mathematical	—	`TwoSidedIdeal` `MvPowerSeries` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MvPowerSeries.instRing` `Preorder.toLE` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `basis` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLE`	—	`TwoSidedIdeal.coe_mk'` `MvPowerSeries.coeff_C` `TwoSidedIdeal.zero_mem` `zero_le` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `eq_top_iff` `MvPowerSeries.coeff_monomial` `MvPowerSeries.coeff_monomial_same` `le_rfl` `basis_le`
`hasBasis_nhds_zero` 📖	mathematical	—	`Filter.HasBasis` `MvPowerSeries` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `nhds` `MvPowerSeries.WithPiTopology.instTopologicalSpace` `MvPowerSeries.instZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `TwoSidedIdeal.setLike` `MvPowerSeries.instRing` `basis`	—	`nhds_pi` `Filter.HasBasis.to_hasBasis` `Filter.HasBasis.pi_self` `IsLinearTopology.hasBasis_twoSidedIdeal` `Nat.instCanonicallyOrderedAdd` `mem_basis_iff` `SetLike.mem_coe` `Finset.le_sup` `Set.Finite.mem_toFinset` `Set.finite_Iic` `TwoSidedIdeal.coe_mk'` `subset_rfl` `Set.instReflSubset`
`instIsLinearTopologyMulOpposite` 📖	mathematical	—	`IsLinearTopology` `MulOpposite` `MvPowerSeries` `MulOpposite.instRing` `MvPowerSeries.instRing` `MvPowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `Semiring.toOppositeModule` `Ring.toSemiring` `MvPowerSeries.WithPiTopology.instTopologicalSpace`	—	`IsLinearTopology.mk_of_hasBasis'` `AddSubgroupClass.toAddSubmonoidClass` `TwoSidedIdeal.instAddSubgroupClass` `hasBasis_nhds_zero` `TwoSidedIdeal.mul_mem_right`
`instIsLinearTopologyOfMulOpposite` 📖	mathematical	—	`IsLinearTopology` `MvPowerSeries` `MvPowerSeries.instRing` `MvPowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `MvPowerSeries.WithPiTopology.instTopologicalSpace`	—	`IsLinearTopology.mk_of_hasBasis'` `AddSubgroupClass.toAddSubmonoidClass` `TwoSidedIdeal.instAddSubgroupClass` `hasBasis_nhds_zero` `TwoSidedIdeal.mul_mem_left`
`isTopologicallyNilpotent_iff_constantCoeff` 📖	mathematical	—	`Filter.Tendsto` `MvPowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MvPowerSeries.WithPiTopology.instTopologicalSpace` `MvPowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsTopologicallyNilpotent` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPowerSeries.constantCoeff`	—	`Filter.Tendsto.comp` `Continuous.tendsto'` `MvPowerSeries.WithPiTopology.continuous_constantCoeff` `MvPowerSeries.constantCoeff_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `isTopologicallyNilpotent_of_constantCoeff`
`isTopologicallyNilpotent_of_constantCoeff` 📖	mathematical	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `MvPowerSeries.constantCoeff`	`MvPowerSeries.WithPiTopology.instTopologicalSpace`	—	`Filter.HasBasis.tendsto_right_iff` `IsLinearTopology.hasBasis_ideal` `Filter.Tendsto.eventually_mem` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Ideal.instIsTwoSided_1` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent` `le_rfl`
`mem_basis_iff` 📖	mathematical	—	`MvPowerSeries` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MvPowerSeries.instRing` `SetLike.instMembership` `TwoSidedIdeal.setLike` `basis` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `MvPowerSeries.coeff`	—	—

---

← Back to Index