Units

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

Statistics

Metric	Count
Definitions piAddUnits, piUnits	2
Theorems val_neg_piAddUnits_apply, val_neg_piAddUnits_symm_apply, val_piAddUnits_apply, val_piAddUnits_symm_apply, apply, val_neg_apply, apply, val_inv_apply, val_inv_piUnits_apply, val_inv_piUnits_symm_apply, val_piUnits_apply, val_piUnits_symm_apply, instSubsingletonAddUnits, instSubsingletonUnits, isAddUnit_iff, isUnit_iff	16
Total	18

AddEquiv

Definitions

Name	Category	Theorems
piAddUnits 📖	CompOp	4 math math: val_neg_piAddUnits_apply, val_piAddUnits_symm_apply, val_neg_piAddUnits_symm_apply, val_piAddUnits_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_neg_piAddUnits_apply 📖	mathematical	—	AddUnits.val AddUnits AddUnits.instNeg DFunLike.coe AddEquiv Pi.addMonoid AddUnits.instAdd Pi.instAdd EquivLike.toFunLike instEquivLike piAddUnits AddUnits.neg	—	—
val_neg_piAddUnits_symm_apply 📖	mathematical	—	AddUnits.val Pi.addMonoid AddUnits AddUnits.instNeg DFunLike.coe AddEquiv Pi.instAdd AddUnits.instAdd EquivLike.toFunLike instEquivLike symm piAddUnits AddUnits.neg	—	—
val_piAddUnits_apply 📖	mathematical	—	AddUnits.val DFunLike.coe AddEquiv AddUnits Pi.addMonoid AddUnits.instAdd Pi.instAdd EquivLike.toFunLike instEquivLike piAddUnits	—	—
val_piAddUnits_symm_apply 📖	mathematical	—	AddUnits.val Pi.addMonoid DFunLike.coe AddEquiv AddUnits Pi.instAdd AddUnits.instAdd EquivLike.toFunLike instEquivLike symm piAddUnits	—	—

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	—	IsAddUnit Pi.addMonoid	—	—	Pi.isAddUnit_iff
val_neg_apply 📖	mathematical	IsAddUnit Pi.addMonoid	AddUnits.val AddUnits AddUnits.instNeg addUnit apply	—	apply AddUnits.neg_eq_val_neg AddEquiv.val_neg_piAddUnits_apply AddUnits.ext

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	—	IsUnit Pi.monoid	—	—	Pi.isUnit_iff
val_inv_apply 📖	mathematical	IsUnit Pi.monoid	Units.val Units Units.instInv unit apply	—	apply Units.inv_eq_val_inv MulEquiv.val_inv_piUnits_apply Units.ext

MulEquiv

Definitions

Name	Category	Theorems
piUnits 📖	CompOp	4 math math: val_piUnits_symm_apply, val_inv_piUnits_apply, val_piUnits_apply, val_inv_piUnits_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_inv_piUnits_apply 📖	mathematical	—	Units.val Units Units.instInv DFunLike.coe MulEquiv Pi.monoid Units.instMul Pi.instMul EquivLike.toFunLike instEquivLike piUnits Units.inv	—	—
val_inv_piUnits_symm_apply 📖	mathematical	—	Units.val Pi.monoid Units Units.instInv DFunLike.coe MulEquiv Pi.instMul Units.instMul EquivLike.toFunLike instEquivLike symm piUnits Units.inv	—	—
val_piUnits_apply 📖	mathematical	—	Units.val DFunLike.coe MulEquiv Units Pi.monoid Units.instMul Pi.instMul EquivLike.toFunLike instEquivLike piUnits	—	—
val_piUnits_symm_apply 📖	mathematical	—	Units.val Pi.monoid DFunLike.coe MulEquiv Units Pi.instMul Units.instMul EquivLike.toFunLike instEquivLike symm piUnits	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingletonAddUnits 📖	mathematical	AddUnits	addMonoid	—	Subsingleton.addUnits_of_isAddUnit isAddUnit_iff isAddUnit_iff_eq_zero
instSubsingletonUnits 📖	mathematical	Units	monoid	—	Subsingleton.units_of_isUnit
isAddUnit_iff 📖	mathematical	—	IsAddUnit addMonoid	—	isAddUnit_iff_exists
isUnit_iff 📖	mathematical	—	IsUnit monoid	—	—

---

← Back to Index