Documentation Verification Report

GroupWithZero

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

Statistics

Metric	Count
Definitions `ContinuousInv₀`, `GroupWithZero`, `inv₀`, `mulLeft₀`, `mulRight₀`, `unitsHomeomorphNeZero`	6
Theorems `comp_div_cases`, `div`, `div_const`, `div₀`, `inv₀`, `zpow₀`, `comp_div_cases`, `div`, `div_const`, `div₀`, `inv₀`, `zpow₀`, `continuousAt_inv₀`, `of_nhds_one`, `div`, `div_const`, `div₀`, `inv₀`, `zpow₀`, `div`, `div_const`, `inv₀`, `zpow₀`, `div`, `div_const`, `inv₀`, `zpow₀`, `tendsto_mul_iff_of_ne_zero`, `coe_mulLeft₀`, `coe_mulRight₀`, `mulLeft₀_symm_apply`, `mulRight₀_symm_apply`, `isEmbedding_val₀`, `continuousAt_zpow₀`, `continuousOn_div`, `continuousOn_inv₀`, `continuousOn_zpow₀`, `map_mul_left_nhds_one₀`, `map_mul_left_nhds₀`, `map_mul_right_nhds_one₀`, `map_mul_right_nhds₀`, `nhds_inv₀`, `nhds_translation_mul_inv₀`, `tendsto_inv_iff₀`, `tendsto_inv₀`	45
Total	51

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_div_cases` 📖	mathematical	`Continuous` `ContinuousAt` `instTopologicalSpaceProd` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `Top.top` `Filter.instTop` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Continuous` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`continuous_iff_continuousAt` `ContinuousAt.comp_div_cases` `continuousAt`
`div` 📖	mathematical	`Continuous`	`Continuous` `Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv₀`
`div_const` 📖	mathematical	`Continuous`	`Continuous` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul_const`
`div₀` 📖	mathematical	`Continuous`	`Continuous` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv₀`
`inv₀` 📖	mathematical	`Continuous`	`Continuous`	—	`continuous_iff_continuousAt` `Filter.Tendsto.inv₀` `tendsto`
`zpow₀` 📖	mathematical	`Continuous`	`Continuous` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	`continuous_iff_continuousAt` `Filter.Tendsto.zpow₀` `tendsto`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_div_cases` 📖	mathematical	`ContinuousAt` `instTopologicalSpaceProd` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `Top.top` `Filter.instTop` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`ContinuousAt` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`eq_1` `div_zero` `Filter.Tendsto.comp` `Filter.Tendsto.prodMk` `tendsto` `continuousAt_id` `Filter.tendsto_top` `comp'` `prodMk` `continuousAt_id'` `div₀`
`div` 📖	mathematical	`ContinuousAt`	`ContinuousAt` `Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`Filter.Tendsto.div`
`div_const` 📖	mathematical	`ContinuousAt`	`ContinuousAt` `DivInvMonoid.toDiv`	—	`Filter.Tendsto.div_const`
`div₀` 📖	mathematical	`ContinuousAt`	`ContinuousAt` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div`
`inv₀` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`Filter.Tendsto.inv₀`
`zpow₀` 📖	mathematical	`ContinuousAt`	`ContinuousAt` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	`Filter.Tendsto.zpow₀`

ContinuousInv₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_inv₀` 📖	mathematical	—	`ContinuousAt`	—	—
`of_nhds_one` 📖	mathematical	`Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `nhds` `InvOneClass.toOne`	`ContinuousInv₀` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`inv_ne_zero` `ContinuousAt.eq_1` `map_mul_left_nhds_one₀` `nhds_translation_mul_inv₀` `Filter.tendsto_map'_iff` `Filter.tendsto_comap_iff` `mul_inv_rev` `mul_inv_cancel_right₀`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`ContinuousOn`	`ContinuousOn` `Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`ContinuousWithinAt.div`
`div_const` 📖	mathematical	`ContinuousOn`	`ContinuousOn` `DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul_const`
`div₀` 📖	mathematical	`ContinuousOn`	`ContinuousOn` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div`
`inv₀` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`ContinuousWithinAt.inv₀`
`zpow₀` 📖	mathematical	`ContinuousOn`	`ContinuousOn` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	`ContinuousWithinAt.zpow₀`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`ContinuousWithinAt`	`ContinuousWithinAt` `Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`Filter.Tendsto.div`
`div_const` 📖	mathematical	`ContinuousWithinAt`	`ContinuousWithinAt` `DivInvMonoid.toDiv`	—	`Filter.Tendsto.div_const`
`inv₀` 📖	mathematical	`ContinuousWithinAt`	`ContinuousWithinAt`	—	`Filter.Tendsto.inv₀`
`zpow₀` 📖	mathematical	`ContinuousWithinAt`	`ContinuousWithinAt` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	`Filter.Tendsto.zpow₀`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_mul_iff_of_ne_zero` 📖	mathematical	`Tendsto` `nhds`	`Tendsto` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `nhds`	—	`mul_div_cancel_right₀` `GroupWithZero.toMulDivCancelClass` `Tendsto.congr'` `Eventually.mono` `Tendsto.eventually_ne` `Tendsto.div` `Tendsto.mul`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `nhds`	—	`div_eq_mul_inv` `mul` `inv₀`
`div_const` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `DivInvMonoid.toDiv` `nhds`	—	`div_eq_mul_inv` `mul_const`
`inv₀` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `tendsto_inv₀`
`zpow₀` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `nhds`	—	`comp` `ContinuousAt.tendsto` `continuousAt_zpow₀`

Homeomorph

Definitions

Name	Category	Theorems
`inv₀` 📖	CompOp	—
`mulLeft₀` 📖	CompOp	2 math math: `mulLeft₀_symm_apply`, `coe_mulLeft₀`
`mulRight₀` 📖	CompOp	2 math math: `coe_mulRight₀`, `mulRight₀_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mulLeft₀` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `mulLeft₀` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	—
`coe_mulRight₀` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `mulRight₀` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	—
`mulLeft₀_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `mulLeft₀` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	—
`mulRight₀_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `mulRight₀` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmbedding_val₀` 📖	mathematical	—	`Topology.IsEmbedding` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `instTopologicalSpaceUnits` `val`	—	`ContinuousOn.mono` `continuousOn_inv₀` `IsUnit.ne_zero` `GroupWithZero.toNontrivial`

(root)

Definitions

Name	Category	Theorems
`ContinuousInv₀` 📖	CompData	8 math math: `IsStrictOrderedRing.toContinuousInv₀`, `NNRat.instContinuousInv₀`, `ContinuousInv₀.of_nhds_one`, `NNReal.instContinuousInv₀`, `NormedDivisionRing.to_continuousInv₀`, `continuousInv₀_of_contMDiffInv₀`, `IsTopologicalDivisionRing.toContinuousInv₀`, `WithZeroTopology.instContinuousInv₀`
`GroupWithZero` 📖	CompData	—
`unitsHomeomorphNeZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_zpow₀` 📖	mathematical	—	`ContinuousAt` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid`	—	`zpow_natCast` `continuousAt_pow` `zpow_negSucc` `LT.lt.not_ge` `ContinuousAt.inv₀` `pow_ne_zero` `isReduced_of_noZeroDivisors` `GroupWithZero.noZeroDivisors`
`continuousOn_div` 📖	mathematical	—	`ContinuousOn` `instTopologicalSpaceProd` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `setOf` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`ContinuousOn.div` `continuousOn_fst` `continuousOn_snd`
`continuousOn_inv₀` 📖	mathematical	—	`ContinuousOn` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`ContinuousAt.continuousWithinAt` `ContinuousInv₀.continuousAt_inv₀`
`continuousOn_zpow₀` 📖	mathematical	—	`ContinuousOn` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`ContinuousAt.continuousWithinAt` `continuousAt_zpow₀`
`map_mul_left_nhds_one₀` 📖	mathematical	—	`Filter.map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`map_mul_left_nhds₀` `mul_one`
`map_mul_left_nhds₀` 📖	mathematical	—	`Filter.map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `nhds`	—	`Homeomorph.map_nhds_eq`
`map_mul_right_nhds_one₀` 📖	mathematical	—	`Filter.map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `nhds` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`map_mul_right_nhds₀` `one_mul`
`map_mul_right_nhds₀` 📖	mathematical	—	`Filter.map` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `nhds`	—	`Homeomorph.map_nhds_eq`
`nhds_inv₀` 📖	mathematical	—	`nhds` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `Filter` `Filter.instInv`	—	`le_antisymm` `Filter.inv_le_iff_le_inv` `inv_inv` `tendsto_inv₀` `inv_ne_zero`
`nhds_translation_mul_inv₀` 📖	mathematical	—	`Filter.comap` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `nhds` `InvOneClass.toOne`	—	`Homeomorph.comap_nhds_eq` `one_mul`
`tendsto_inv_iff₀` 📖	mathematical	—	`Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `nhds`	—	`nhds_inv₀` `inv_inv`
`tendsto_inv₀` 📖	mathematical	—	`Filter.Tendsto` `nhds`	—	`ContinuousInv₀.continuousAt_inv₀`

---

← Back to Index