Equiv

📁 Source: Mathlib/Algebra/AddConstMap/Equiv.lean

Statistics

Metric	Count
Definitions `AddConstEquiv`, `symm_apply`, `equivUnits`, `instDiv`, `instEquivLike`, `instGroup`, `instInv`, `instMul`, `instOne`, `instPowInt`, `instPowNat`, `refl`, `toAddConstMap`, `toAddConstMapHom`, `toEquiv`, `toPerm`, `trans`, `«term_≃+c[_,_]_»`	18
Theorems `coe_symm_toEquiv`, `coe_toEquiv`, `coe_val_equivUnits_apply`, `coe_val_inv_equivUnits_apply`, `equivUnits_symm_apply_apply`, `equivUnits_symm_apply_symm_apply`, `ext`, `ext_iff`, `instAddConstMapClass`, `map_add_const'`, `refl_apply`, `refl_toEquiv`, `refl_trans`, `self_trans_symm`, `symm_refl`, `symm_symm`, `symm_trans_self`, `toAddConstMapHom_apply`, `toEquiv_inj`, `toEquiv_injective`, `toEquiv_symm`, `toEquiv_trans`, `toPerm_apply`, `trans_apply`, `trans_refl`, `trans_toEquiv`	26
Total	44

AddConstEquiv

Definitions

Name	Category	Theorems
`equivUnits` 📖	CompOp	4 math math: `coe_val_inv_equivUnits_apply`, `equivUnits_symm_apply_apply`, `equivUnits_symm_apply_symm_apply`, `coe_val_equivUnits_apply`
`instDiv` 📖	CompOp	—
`instEquivLike` 📖	CompOp	10 math math: `trans_apply`, `refl_apply`, `ext_iff`, `coe_symm_toEquiv`, `coe_val_inv_equivUnits_apply`, `equivUnits_symm_apply_apply`, `coe_toEquiv`, `instAddConstMapClass`, `equivUnits_symm_apply_symm_apply`, `coe_val_equivUnits_apply`
`instGroup` 📖	CompOp	3 math math: `toAddConstMapHom_apply`, `coe_val_inv_equivUnits_apply`, `toPerm_apply`
`instInv` 📖	CompOp	—
`instMul` 📖	CompOp	4 math math: `coe_val_inv_equivUnits_apply`, `equivUnits_symm_apply_apply`, `equivUnits_symm_apply_symm_apply`, `coe_val_equivUnits_apply`
`instOne` 📖	CompOp	—
`instPowInt` 📖	CompOp	—
`instPowNat` 📖	CompOp	—
`refl` 📖	CompOp	7 math math: `refl_apply`, `symm_trans_self`, `symm_refl`, `self_trans_symm`, `refl_toEquiv`, `trans_refl`, `refl_trans`
`toAddConstMap` 📖	CompOp	1 math math: `toAddConstMapHom_apply`
`toAddConstMapHom` 📖	CompOp	1 math math: `toAddConstMapHom_apply`
`toEquiv` 📖	CompOp	10 math math: `toEquiv_injective`, `coe_symm_toEquiv`, `toEquiv_inj`, `toEquiv_symm`, `toEquiv_trans`, `toPerm_apply`, `map_add_const'`, `coe_toEquiv`, `trans_toEquiv`, `refl_toEquiv`
`toPerm` 📖	CompOp	1 math math: `toPerm_apply`
`trans` 📖	CompOp	7 math math: `trans_apply`, `symm_trans_self`, `toEquiv_trans`, `self_trans_symm`, `trans_toEquiv`, `trans_refl`, `refl_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_symm_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `AddConstEquiv` `instEquivLike` `symm`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `AddConstEquiv` `instEquivLike`	—	—
`coe_val_equivUnits_apply` 📖	mathematical	—	`DFunLike.coe` `AddConstMap` `AddConstMap.instFunLike` `Units.val` `AddConstMap.instMonoid` `MulEquiv` `AddConstEquiv` `Units` `instMul` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `equivUnits` `instEquivLike`	—	—
`coe_val_inv_equivUnits_apply` 📖	mathematical	—	`DFunLike.coe` `AddConstMap` `AddConstMap.instFunLike` `Units.val` `AddConstMap.instMonoid` `Units` `Units.instInv` `MulEquiv` `AddConstEquiv` `instMul` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `equivUnits` `instEquivLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instGroup`	—	—
`equivUnits_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike` `MulEquiv` `Units` `AddConstMap` `AddConstMap.instMonoid` `Units.instMul` `instMul` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnits` `AddConstMap.instFunLike` `Units.val`	—	—
`equivUnits_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `MulEquiv` `Units` `AddConstMap` `AddConstMap.instMonoid` `Units.instMul` `instMul` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnits` `AddConstMap.instFunLike` `Units.val` `Units.instInv`	—	—
`ext` 📖	—	`DFunLike.coe` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`instAddConstMapClass` 📖	mathematical	—	`AddConstMapClass` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`map_add_const'`
`map_add_const'` 📖	mathematical	—	`Equiv.toFun` `toEquiv`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`refl_toEquiv` 📖	mathematical	—	`toEquiv` `refl` `Equiv.refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	—
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`toEquiv_injective` `Equiv.self_trans_symm`
`symm_refl` 📖	mathematical	—	`symm` `refl`	—	—
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`toEquiv_injective` `Equiv.symm_trans_self`
`toAddConstMapHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `AddConstEquiv` `AddConstMap` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `AddConstMap.instMonoid` `MonoidHom.instFunLike` `toAddConstMapHom` `toAddConstMap`	—	—
`toEquiv_inj` 📖	mathematical	—	`toEquiv`	—	`toEquiv_injective`
`toEquiv_injective` 📖	mathematical	—	`AddConstEquiv` `Equiv` `toEquiv`	—	—
`toEquiv_symm` 📖	mathematical	—	`toEquiv` `symm` `Equiv.symm`	—	—
`toEquiv_trans` 📖	mathematical	—	`toEquiv` `trans` `Equiv.trans`	—	—
`toPerm_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `AddConstEquiv` `Equiv.Perm` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `toPerm` `toEquiv`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `AddConstEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	—
`trans_toEquiv` 📖	mathematical	—	`toEquiv` `trans` `Equiv.trans`	—	—

AddConstEquiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

AddConstMap

Definitions

Name	Category	Theorems
`«term_≃+c[_,_]_»` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`AddConstEquiv` 📖	CompData	13 math math: `AddConstEquiv.trans_apply`, `AddConstEquiv.refl_apply`, `AddConstEquiv.ext_iff`, `AddConstEquiv.toEquiv_injective`, `AddConstEquiv.coe_symm_toEquiv`, `AddConstEquiv.toAddConstMapHom_apply`, `AddConstEquiv.coe_val_inv_equivUnits_apply`, `AddConstEquiv.toPerm_apply`, `AddConstEquiv.equivUnits_symm_apply_apply`, `AddConstEquiv.coe_toEquiv`, `AddConstEquiv.instAddConstMapClass`, `AddConstEquiv.equivUnits_symm_apply_symm_apply`, `AddConstEquiv.coe_val_equivUnits_apply`

---

← Back to Index