Documentation Verification Report

Units

📁 Source: Mathlib/Topology/Algebra/Group/Units.lean

Statistics

Metric	Count
Definitions `piAddUnits`, `piUnits`, `mapContinuousMulEquiv`	3
Theorems `isOpen_addUnits`, `isOpen_units`, `mapContinuousMulEquiv_apply`, `symm_mapContinuousMulEquiv`, `toMulEquiv_mapContinuousMulEquiv`	5
Total	8

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_addUnits` 📖	mathematical	`IsOpen` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `instSetLike`	`AddUnits` `AddUnits.instTopologicalSpaceAddUnits` `AddSubgroup` `AddUnits.instAddGroup` `AddSubgroup.instSetLike` `addUnits`	—	`IsOpen.inter` `IsOpen.preimage` `AddUnits.continuous_val` `AddUnits.continuous_coe_neg`

ContinuousAddEquiv

Definitions

Name	Category	Theorems
`piAddUnits` 📖	CompOp	—

ContinuousMulEquiv

Definitions

Name	Category	Theorems
`piUnits` 📖	CompOp	—

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_units` 📖	mathematical	`IsOpen` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `instSetLike`	`Units` `Units.instTopologicalSpaceUnits` `Subgroup` `Units.instGroup` `Subgroup.instSetLike` `units`	—	`IsOpen.inter` `IsOpen.preimage` `Units.continuous_val` `Units.continuous_coe_inv`

Units

Definitions

Name	Category	Theorems
`mapContinuousMulEquiv` 📖	CompOp	3 math math: `symm_mapContinuousMulEquiv`, `toMulEquiv_mapContinuousMulEquiv`, `mapContinuousMulEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapContinuousMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `Units` `instTopologicalSpaceUnits` `instMul` `EquivLike.toFunLike` `ContinuousMulEquiv.instEquivLike` `mapContinuousMulEquiv` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `map` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `Monoid.toMulOneClass` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquivClass.toMulEquiv`	—	—
`symm_mapContinuousMulEquiv` 📖	mathematical	—	`ContinuousMulEquiv.symm` `Units` `instTopologicalSpaceUnits` `instMul` `mapContinuousMulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`toMulEquiv_mapContinuousMulEquiv` 📖	mathematical	—	`MulEquivClass.toMulEquiv` `ContinuousMulEquiv` `Units` `instTopologicalSpaceUnits` `instMul` `ContinuousMulEquiv.instEquivLike` `ContinuousMulEquiv.instMulEquivClass` `mapContinuousMulEquiv` `mapEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`ContinuousMulEquiv.instMulEquivClass`

---

← Back to Index