Documentation Verification Report

Field

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

Statistics

Metric	Count
Definitions `IsTopologicalDivisionRing`, `unitsHomeomorphPos`, `topologicalClosure`, `affineHomeomorph`	4
Theorems `finite_of_compactSpace_of_t2Space`, `tendsto_cocompact_mul_left₀`, `tendsto_cocompact_mul_right₀`, `inv`, `eq_of_sq_eq`, `eq_one_or_eq_neg_one_of_sq_eq`, `eq_or_eq_neg_of_sq_eq`, `toContinuousInv₀`, `toIsTopologicalRing`, `unitsHomeomorphPos_apply_coe`, `val_inv_unitsHomeomorphPos_symm_apply_coe`, `val_unitsHomeomorphPos_symm_apply_coe`, `continuousSMul`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `topologicalClosure_minimal`, `affineHomeomorph_apply`, `affineHomeomorph_image_Icc`, `affineHomeomorph_image_Ico`, `affineHomeomorph_image_Ioc`, `affineHomeomorph_image_Ioo`, `affineHomeomorph_symm_apply`	22
Total	26

DivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_compactSpace_of_t2Space` 📖	mathematical	—	`Finite`	—	`discreteTopology_iff_isOpen_singleton_zero` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `GroupWithZero.isOpen_singleton_zero` `IsTopologicalSemiring.toContinuousMul` `T2Space.t1Space` `finite_of_compact_of_discrete`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_cocompact_mul_left₀` 📖	mathematical	—	`Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `cocompact`	—	`tendsto_cocompact_mul_left` `inv_mul_cancel₀`
`tendsto_cocompact_mul_right₀` 📖	mathematical	—	`Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `cocompact`	—	`tendsto_cocompact_mul_right` `mul_inv_cancel₀`

IsLocalMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Eventually` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `nhds`	`IsLocalMax` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`Filter.mp_mem` `Filter.univ_mem'` `inv_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Filter.Eventually.self_of_nhds`

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_sq_eq` 📖	—	`IsPreconnected` `ContinuousOn` `Set.EqOn` `Monoid.toNatPow` `Pi.monoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Set` `Set.instMembership`	—	—	`eq_or_eq_neg_of_sq_eq` `Pi.neg_apply` `neg_eq_iff_add_eq_zero` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `mul_eq_zero` `IsDomain.to_noZeroDivisors` `Field.isDomain`
`eq_one_or_eq_neg_one_of_sq_eq` 📖	mathematical	`IsPreconnected` `ContinuousOn` `Set.EqOn` `Monoid.toNatPow` `Pi.monoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`eqOn_const_of_mapsTo` `Set.Finite.isDiscrete` `Set.toFinite` `Finite.Set.finite_insert` `Finite.of_fintype`
`eq_or_eq_neg_of_sq_eq` 📖	mathematical	`IsPreconnected` `ContinuousOn` `Set.EqOn` `Monoid.toNatPow` `Pi.monoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`div_pow` `div_eq_one_iff_eq` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Field.isDomain` `div_eq_iff` `one_mul` `neg_mul` `eq_one_or_eq_neg_one_of_sq_eq` `ContinuousOn.div`

IsTopologicalDivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContinuousInv₀` 📖	mathematical	—	`ContinuousInv₀` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	—
`toIsTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	—

Nonneg

Definitions

Name	Category	Theorems
`unitsHomeomorphPos` 📖	CompOp	3 math math: `val_unitsHomeomorphPos_symm_apply_coe`, `val_inv_unitsHomeomorphPos_symm_apply_coe`, `unitsHomeomorphPos_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unitsHomeomorphPos_apply_coe` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DFunLike.coe` `Homeomorph` `Units` `Preorder.toLE` `MonoidWithZero.toMonoid` `monoidWithZero` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono` `Units.instTopologicalSpaceUnits` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `unitsHomeomorphPos` `Units.val`	—	`IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono`
`val_inv_unitsHomeomorphPos_symm_apply_coe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Units.val` `MonoidWithZero.toMonoid` `monoidWithZero` `Units` `Units.instInv` `DFunLike.coe` `Homeomorph` `Preorder.toLT` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono` `instTopologicalSpaceSubtype` `Units.instTopologicalSpaceUnits` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `unitsHomeomorphPos` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero`	—	`IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono`
`val_unitsHomeomorphPos_symm_apply_coe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Units.val` `MonoidWithZero.toMonoid` `monoidWithZero` `DFunLike.coe` `Homeomorph` `Preorder.toLT` `Units` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono` `instTopologicalSpaceSubtype` `Units.instTopologicalSpaceUnits` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `unitsHomeomorphPos`	—	`IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toPosMulMono`

Subfield

Definitions

Name	Category	Theorems
`topologicalClosure` 📖	CompOp	3 math math: `topologicalClosure_minimal`, `isClosed_topologicalClosure`, `le_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `Subfield` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `toDivisionRing` `MulAction.toSemigroupAction` `Submonoid.instMulActionSubtypeMem` `Ring.toSemiring` `DivisionRing.toRing` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `instTopologicalSpaceSubtype`	—	`Subring.continuousSMul`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subfield` `Field.toDivisionRing` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`Subfield` `Field.toDivisionRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`topologicalClosure_minimal` 📖	mathematical	`Subfield` `Field.toDivisionRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`

(root)

Definitions

Name	Category	Theorems
`IsTopologicalDivisionRing` 📖	CompData	6 math math: `instIsTopologicalDivisionRingReal`, `IsStrictOrderedRing.toIsTopologicalDivisionRing`, `UniformSpace.Completion.instIsTopologicalDivisionRing`, `NormedDivisionRing.to_isTopologicalDivisionRing`, `IsNonarchimedeanLocalField.instIsTopologicalDivisionRing`, `Valued.isTopologicalDivisionRing`
`affineHomeomorph` 📖	CompOp	7 math math: `affineHomeomorph_image_Ioc`, `affineHomeomorph_image_Ico`, `affineHomeomorph_symm_apply`, `affineHomeomorph_image_I`, `affineHomeomorph_image_Ioo`, `affineHomeomorph_image_Icc`, `affineHomeomorph_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `affineHomeomorph` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toMul`	—	—
`affineHomeomorph_image_Icc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `affineHomeomorph` `LT.lt.ne'` `Set.Icc` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`LT.lt.ne'` `Set.image_congr` `Set.image_affine_Icc'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `AddGroup.existsAddOfLE`
`affineHomeomorph_image_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `affineHomeomorph` `LT.lt.ne'` `Set.Ico` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`LT.lt.ne'` `Set.image_congr` `Set.image_affine_Ico` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `AddGroup.existsAddOfLE`
`affineHomeomorph_image_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `affineHomeomorph` `LT.lt.ne'` `Set.Ioc` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`LT.lt.ne'` `Set.image_congr` `Set.image_affine_Ioc` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `AddGroup.existsAddOfLE`
`affineHomeomorph_image_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `affineHomeomorph` `LT.lt.ne'` `Set.Ioo` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`LT.lt.ne'` `Set.image_congr` `Set.image_affine_Ioo` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `AddGroup.existsAddOfLE`
`affineHomeomorph_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `affineHomeomorph` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	—

---

← Back to Index