Center

📁 Source: Mathlib/Algebra/GroupWithZero/Action/Center.lean

Statistics

Metric	Count
Definitions centerUnitsEquivUnitsCenter	1
Theorems val_centerUnitsEquivUnitsCenter_apply_coe, val_centerUnitsEquivUnitsCenter_symm_apply_coe	2
Total	3

Subgroup

Definitions

Name	Category	Theorems
centerUnitsEquivUnitsCenter 📖	CompOp	2 math math: val_centerUnitsEquivUnitsCenter_symm_apply_coe, val_centerUnitsEquivUnitsCenter_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_centerUnitsEquivUnitsCenter_apply_coe 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike Submonoid.center Units.val Submonoid.toMonoid MonoidWithZero.toMonoid DFunLike.coe MulEquiv Units Subgroup Units.instGroup instSetLike center mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike centerUnitsEquivUnitsCenter	—	—
val_centerUnitsEquivUnitsCenter_symm_apply_coe 📖	mathematical	—	Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero Units Submonoid Units.instMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.center DFunLike.coe MulEquiv MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Submonoid.toMonoid Subgroup Units.instGroup instSetLike center Units.instMul mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm centerUnitsEquivUnitsCenter Monoid.toMulOneClass	—	—

---

← Back to Index