Documentation Verification Report

LinearTopology

📁 Source: Mathlib/Topology/Algebra/LinearTopology.lean

Statistics

Metric	Count
Definitions `IsLinearTopology`	1
Theorems `isLinearTopology_iff`, `hasBasis_ideal`, `hasBasis_open_ideal`, `hasBasis_open_subbimodule`, `hasBasis_open_submodule`, `hasBasis_open_twoSidedIdeal`, `hasBasis_right_ideal`, `hasBasis_subbimodule`, `hasBasis_submodule`, `hasBasis_submodule'`, `hasBasis_twoSidedIdeal`, `instMulOpposite`, `instOfDiscreteTopology`, `mk_of_hasBasis`, `mk_of_hasBasis'`, `tendsto_mul_zero_of_left`, `tendsto_mul_zero_of_right`, `tendsto_smul_zero`, `isLinearTopology_iff_hasBasis_ideal`, `isLinearTopology_iff_hasBasis_open_ideal`, `isLinearTopology_iff_hasBasis_open_submodule`, `isLinearTopology_iff_hasBasis_open_twoSidedIdeal`, `isLinearTopology_iff_hasBasis_submodule`, `isLinearTopology_iff_hasBasis_twoSidedIdeal`	24
Total	25

IsCentralScalar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLinearTopology_iff` 📖	mathematical	—	`IsLinearTopology` `MulOpposite` `MulOpposite.instRing`	—	`IsLinearTopology.mk_of_hasBasis'` `Submodule.addSubmonoidClass` `IsLinearTopology.hasBasis_submodule` `Submodule.smul_mem` `op_smul_eq_smul` `unop_smul_eq_smul`

IsLinearTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis_ideal` 📖	mathematical	—	`Filter.HasBasis` `Ideal` `Ring.toSemiring` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`hasBasis_submodule`
`hasBasis_open_ideal` 📖	mathematical	—	`Filter.HasBasis` `Ideal` `Ring.toSemiring` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsOpen` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`hasBasis_open_submodule`
`hasBasis_open_subbimodule` 📖	mathematical	—	`Filter.HasBasis` `AddSubgroup` `AddCommGroup.toAddGroup` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `IsOpen` `SetLike.coe` `AddSubgroup.instSetLike`	—	`Filter.HasBasis.congr` `hasBasis_subbimodule` `AddSubgroup.isOpen_of_mem_nhds` `IsOpen.mem_nhds` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass`
`hasBasis_open_submodule` 📖	mathematical	—	`Filter.HasBasis` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `IsOpen` `SetLike.coe` `Submodule.setLike`	—	`Filter.HasBasis.congr` `hasBasis_submodule` `AddSubgroup.isOpen_of_mem_nhds` `IsOpen.mem_nhds` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`hasBasis_open_twoSidedIdeal` 📖	mathematical	—	`Filter.HasBasis` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `IsOpen` `SetLike.coe` `TwoSidedIdeal.setLike`	—	`Filter.HasBasis.congr` `hasBasis_twoSidedIdeal` `AddSubgroup.isOpen_of_mem_nhds` `IsOpen.mem_nhds` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `TwoSidedIdeal.instAddSubgroupClass`
`hasBasis_right_ideal` 📖	mathematical	—	`Filter.HasBasis` `Submodule` `MulOpposite` `MulOpposite.instSemiring` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toOppositeModule` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `Submodule.setLike`	—	`hasBasis_submodule`
`hasBasis_subbimodule` 📖	mathematical	—	`Filter.HasBasis` `AddSubgroup` `AddCommGroup.toAddGroup` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `AddSubgroup.instSetLike`	—	`Filter.HasBasis.to_hasBasis` `hasBasis_submodule` `Filter.HasBasis.mem_iff` `Set.subset_univ` `Set.smul_subset_iff` `Submodule.smul_mem` `subset_trans` `Set.instIsTransSubset` `Set.smul_subset_smul_left` `Set.union_subset` `Set.smul_union` `SemigroupAction.mul_smul` `Set.union_subset_union` `subset_refl` `Set.instReflSubset` `Set.smul_subset_smul` `Set.union_self` `Set.subset_union_right` `SMulCommClass.smul_comm` `Set.smulCommClass` `AddSubgroup.closure_induction` `AddSubgroup.subset_closure` `Set.smul_mem_smul` `smul_zero` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass` `smul_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `smul_neg` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `AddSubgroup.closure_le` `Set.subset_union_left` `Filter.mem_of_superset` `subset_rfl`
`hasBasis_submodule` 📖	mathematical	—	`Filter.HasBasis` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `Submodule.setLike`	—	`hasBasis_submodule'`
`hasBasis_submodule'` 📖	mathematical	—	`Filter.HasBasis` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `Submodule.setLike`	—	—
`hasBasis_twoSidedIdeal` 📖	mathematical	—	`Filter.HasBasis` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `TwoSidedIdeal.setLike`	—	`Filter.HasBasis.to_hasBasis` `hasBasis_subbimodule` `SMulCommClass.opposite_mid` `IsScalarTower.left` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `TwoSidedIdeal.coe_mk'` `Set.instReflSubset` `TwoSidedIdeal.mul_mem_left` `TwoSidedIdeal.mul_mem_right` `subset_rfl`
`instMulOpposite` 📖	mathematical	—	`IsLinearTopology` `MulOpposite` `MulOpposite.instRing` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toOppositeModule` `Ring.toSemiring`	—	`IsCentralScalar.isLinearTopology_iff` `CommSemigroup.isCentralScalar`
`instOfDiscreteTopology` 📖	mathematical	—	`IsLinearTopology`	—	`nhds_discrete` `Filter.hasBasis_pure` `mk_of_hasBasis` `Submodule.smulMemClass` `Submodule.addSubmonoidClass`
`mk_of_hasBasis` 📖	mathematical	`Filter.HasBasis` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SetLike.coe`	`IsLinearTopology`	—	`mk_of_hasBasis'` `SMulMemClass.smul_mem`
`mk_of_hasBasis'` 📖	mathematical	`Filter.HasBasis` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SetLike.coe` `SetLike.instMembership` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`IsLinearTopology`	—	`Filter.HasBasis.to_hasBasis` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Filter.HasBasis.mem_of_mem` `subset_rfl` `Set.instReflSubset` `Filter.HasBasis.mem_iff`
`tendsto_mul_zero_of_left` 📖	mathematical	`Filter.Tendsto` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`tendsto_smul_zero`
`tendsto_mul_zero_of_right` 📖	mathematical	`Filter.Tendsto` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`tendsto_smul_zero`
`tendsto_smul_zero` 📖	mathematical	`Filter.Tendsto` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Filter.HasBasis.tendsto_right_iff` `hasBasis_submodule` `Filter.mp_mem` `Filter.univ_mem'` `Submodule.smul_mem`

(root)

Definitions

Name	Category	Theorems
`IsLinearTopology` 📖	CompData	14 math math: `isLinearTopology_iff_hasBasis_open_twoSidedIdeal`, `IsLinearTopology.mk_of_hasBasis'`, `WithIdealFilter.instIsLinearTopology`, `MvPowerSeries.LinearTopology.instIsLinearTopologyMulOpposite`, `IsLinearTopology.instOfDiscreteTopology`, `isLinearTopology_iff_hasBasis_ideal`, `IsLinearTopology.instMulOpposite`, `MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite`, `IsLinearTopology.mk_of_hasBasis`, `isLinearTopology_iff_hasBasis_open_ideal`, `IsCentralScalar.isLinearTopology_iff`, `isLinearTopology_iff_hasBasis_open_submodule`, `isLinearTopology_iff_hasBasis_submodule`, `isLinearTopology_iff_hasBasis_twoSidedIdeal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLinearTopology_iff_hasBasis_ideal` 📖	mathematical	—	`IsLinearTopology` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Filter.HasBasis` `Ideal` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isLinearTopology_iff_hasBasis_submodule`
`isLinearTopology_iff_hasBasis_open_ideal` 📖	mathematical	—	`IsLinearTopology` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Filter.HasBasis` `Ideal` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsOpen` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isLinearTopology_iff_hasBasis_open_submodule` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring`
`isLinearTopology_iff_hasBasis_open_submodule` 📖	mathematical	—	`IsLinearTopology` `Filter.HasBasis` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `IsOpen` `SetLike.coe` `Submodule.setLike`	—	`IsLinearTopology.hasBasis_open_submodule` `IsLinearTopology.mk_of_hasBasis` `Submodule.smulMemClass` `Submodule.addSubmonoidClass`
`isLinearTopology_iff_hasBasis_open_twoSidedIdeal` 📖	mathematical	—	`IsLinearTopology` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `MulOpposite` `MulOpposite.instRing` `Semiring.toOppositeModule` `Filter.HasBasis` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `IsOpen` `SetLike.coe` `TwoSidedIdeal.setLike`	—	`IsLinearTopology.hasBasis_open_twoSidedIdeal` `IsLinearTopology.mk_of_hasBasis'` `AddSubgroupClass.toAddSubmonoidClass` `TwoSidedIdeal.instAddSubgroupClass` `TwoSidedIdeal.mul_mem_left` `TwoSidedIdeal.mul_mem_right`
`isLinearTopology_iff_hasBasis_submodule` 📖	mathematical	—	`IsLinearTopology` `Filter.HasBasis` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `Submodule.setLike`	—	`IsLinearTopology.hasBasis_submodule` `IsLinearTopology.mk_of_hasBasis` `Submodule.smulMemClass` `Submodule.addSubmonoidClass`
`isLinearTopology_iff_hasBasis_twoSidedIdeal` 📖	mathematical	—	`IsLinearTopology` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `MulOpposite` `MulOpposite.instRing` `Semiring.toOppositeModule` `Filter.HasBasis` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Set` `Filter` `Filter.instMembership` `SetLike.coe` `TwoSidedIdeal.setLike`	—	`IsLinearTopology.hasBasis_twoSidedIdeal` `IsLinearTopology.mk_of_hasBasis'` `AddSubgroupClass.toAddSubmonoidClass` `TwoSidedIdeal.instAddSubgroupClass` `TwoSidedIdeal.mul_mem_left` `TwoSidedIdeal.mul_mem_right`

---

← Back to Index