Documentation Verification Report

Equiv

📁 Source: Mathlib/Algebra/GroupWithZero/Units/Equiv.lean

Statistics

Metric	Count
Definitions `divLeft₀`, `divRight₀`, `mulLeft₀`, `mulRight₀`, `unitsEquivNeZero`	5
Theorems `divLeft₀_apply`, `divLeft₀_symm_apply`, `divRight₀_apply`, `divRight₀_symm_apply`, `mulLeft₀_apply`, `mulLeft₀_symm_apply`, `mulRight₀_apply`, `mulRight₀_symm_apply`, `mulLeft_bijective₀`, `mulRight_bijective₀`, `unitsEquivNeZero_apply_coe`, `unitsEquivNeZero_symm_apply`	12
Total	17

Equiv

Definitions

Name	Category	Theorems
`divLeft₀` 📖	CompOp	2 math math: `divLeft₀_apply`, `divLeft₀_symm_apply`
`divRight₀` 📖	CompOp	2 math math: `divRight₀_symm_apply`, `divRight₀_apply`
`mulLeft₀` 📖	CompOp	3 math math: `mulLeft₀_apply`, `mulLeft₀_symm_apply`, `MeasurableEquiv.toEquiv_mulLeft₀`
`mulRight₀` 📖	CompOp	3 math math: `MeasurableEquiv.toEquiv_mulRight₀`, `mulRight₀_apply`, `mulRight₀_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divLeft₀_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `divLeft₀` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero`	—	—
`divLeft₀_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `divLeft₀` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero`	—	—
`divRight₀_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `divRight₀` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	—
`divRight₀_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `divRight₀` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	—
`mulLeft₀_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `mulLeft₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	—
`mulLeft₀_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `mulLeft₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_inv_eq_inv_val`
`mulRight₀_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `mulRight₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	—
`mulRight₀_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `mulRight₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_inv_eq_inv_val`

(root)

Definitions

Name	Category	Theorems
`unitsEquivNeZero` 📖	CompOp	2 math math: `unitsEquivNeZero_symm_apply`, `unitsEquivNeZero_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_bijective₀` 📖	mathematical	—	`Function.Bijective` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`Equiv.bijective`
`mulRight_bijective₀` 📖	mathematical	—	`Function.Bijective` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`Equiv.bijective`
`unitsEquivNeZero_apply_coe` 📖	mathematical	—	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `DFunLike.coe` `Equiv` `Units` `MonoidWithZero.toMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `unitsEquivNeZero` `Units.val`	—	—
`unitsEquivNeZero_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `Units` `MonoidWithZero.toMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `unitsEquivNeZero`	—	—

---

← Back to Index