Units

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

Statistics

Metric	Count
Definitions coeUnits, mkUnit, unitsEquiv	3
Theorems coe_unitsEquiv_apply, eventualy_isUnit_of_isUnit, isUnit_iff, isUnit_of_eventually_isUnit, unitsEquiv_apply	5
Total	8

RestrictedProduct

Definitions

Name	Category	Theorems
coeUnits 📖	CompOp	—
mkUnit 📖	CompOp	—
unitsEquiv 📖	CompOp	2 math math: coe_unitsEquiv_apply, unitsEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_unitsEquiv_apply 📖	mathematical	SubmonoidClass Monoid.toMulOneClass	Filter.Eventually Set Set.instMembership DFunLike.coe MulEquiv Units RestrictedProduct SetLike.coe instMonoidCoeOfSubmonoidClass Subgroup Units.instGroup Subgroup.instSetLike Submonoid.units Submonoid.ofClass Units.instMul instMulCoeOfMulMemClass SubmonoidClass.toMulMemClass Units.instMulOneClass SubgroupClass.toSubmonoidClass Units.instDivInvMonoid Subgroup.instSubgroupClass EquivLike.toFunLike MulEquiv.instEquivLike unitsEquiv instDFunLike	—	SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass
eventualy_isUnit_of_isUnit 📖	mathematical	SubmonoidClass Monoid.toMulOneClass IsUnit RestrictedProduct SetLike.coe instMonoidCoeOfSubmonoidClass	IsUnit DFunLike.coe RestrictedProduct SetLike.coe instDFunLike Filter.Eventually SetLike.instMembership SubmonoidClass.toMonoid	—	Filter.mp_mem Filter.univ_mem' MulMemClass.mul_mem
isUnit_iff 📖	mathematical	SubmonoidClass Monoid.toMulOneClass	IsUnit RestrictedProduct SetLike.coe instMonoidCoeOfSubmonoidClass DFunLike.coe instDFunLike Filter.Eventually SetLike.instMembership SubmonoidClass.toMonoid	—	eventualy_isUnit_of_isUnit isUnit_of_eventually_isUnit
isUnit_of_eventually_isUnit 📖	mathematical	SubmonoidClass Monoid.toMulOneClass IsUnit DFunLike.coe RestrictedProduct SetLike.coe instDFunLike Filter.Eventually SetLike.instMembership SubmonoidClass.toMonoid	IsUnit RestrictedProduct SetLike.coe instMonoidCoeOfSubmonoidClass	—	isUnit_iff_exists Filter.mp_mem Filter.univ_mem' IsUnit.mul_val_inv Units.eq_inv_of_mul_eq_one_left IsUnit.val_inv_mul
unitsEquiv_apply 📖	mathematical	SubmonoidClass Monoid.toMulOneClass	Units.val DFunLike.coe RestrictedProduct Units SetLike.coe Subgroup Units.instGroup Subgroup.instSetLike Submonoid.units Submonoid.ofClass instDFunLike MulEquiv instMonoidCoeOfSubmonoidClass Units.instMul instMulCoeOfMulMemClass SubmonoidClass.toMulMemClass Units.instMulOneClass SubgroupClass.toSubmonoidClass Units.instDivInvMonoid Subgroup.instSubgroupClass EquivLike.toFunLike MulEquiv.instEquivLike unitsEquiv	—	SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass

---

← Back to Index