Ext

📁 Source: Mathlib/Algebra/Group/Ext.lean

Statistics

Metric	Count
Definitions	0
Theorems ext, ext_iff, toAddCommMonoid_injective, ext, ext_iff, toAddLeftCancelMonoid_injective, ext, ext_iff, toAddGroup_injective, ext, ext_iff, toAddMonoid_injective, ext, ext_iff, toSubNegAddMonoid_injective, ext, ext_iff, toAddMonoid_injective, ext, ext_iff, ext, ext_iff, toAddMonoid_injective, ext, ext_iff, toCommMonoid_injective, ext, ext_iff, toLeftCancelMonoid_injective, ext, ext_iff, toGroup_injective, ext, ext_iff, toMonoid_injective, ext, ext_iff, ext, ext_iff, toDivInvMonoid_injective, ext, ext_iff, toMonoid_injective, ext, ext_iff, ext, ext_iff, toMonoid_injective, ext, ext_iff	50
Total	50

AddCancelCommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toAddCommMonoid	—	—	toAddCommMonoid_injective AddCommMonoid.ext
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toAddCommMonoid	—	ext
toAddCommMonoid_injective 📖	mathematical	—	AddCancelCommMonoid AddCommMonoid toAddCommMonoid	—	—

AddCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid toAddRightCancelMonoid	—	—	toAddLeftCancelMonoid_injective AddLeftCancelMonoid.ext
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid toAddRightCancelMonoid	—	ext
toAddLeftCancelMonoid_injective 📖	mathematical	—	AddCancelMonoid AddLeftCancelMonoid toAddLeftCancelMonoid	—	—

AddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup	—	—	toAddGroup_injective AddGroup.ext
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup	—	ext
toAddGroup_injective 📖	mathematical	—	AddCommGroup AddGroup toAddGroup	—	—

AddCommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	—	toAddMonoid_injective AddMonoid.ext
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	ext
toAddMonoid_injective 📖	mathematical	—	AddCommMonoid AddMonoid toAddMonoid	—	—

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid toSubNegMonoid	—	—	AddMonoid.ext toSubNegAddMonoid_injective SubNegMonoid.ext AddMonoidHom.map_neg
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid toSubNegMonoid	—	ext
toSubNegAddMonoid_injective 📖	mathematical	—	AddGroup SubNegMonoid toSubNegMonoid	—	—

AddLeftCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	—	toAddMonoid_injective AddMonoid.ext
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	ext
toAddMonoid_injective 📖	mathematical	—	AddLeftCancelMonoid AddMonoid toAddMonoid	—	—

AddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero toAddZeroClass	—	—	AddZeroClass.ext AddMonoidHom.map_nsmul
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero toAddZeroClass	—	ext

AddRightCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	—	toAddMonoid_injective AddMonoid.ext
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	ext
toAddMonoid_injective 📖	mathematical	—	AddRightCancelMonoid AddMonoid toAddMonoid	—	—

CancelCommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid toCommMonoid	—	—	toCommMonoid_injective CommMonoid.ext
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid toCommMonoid	—	ext
toCommMonoid_injective 📖	mathematical	—	CancelCommMonoid CommMonoid toCommMonoid	—	—

CancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid toRightCancelMonoid	—	—	toLeftCancelMonoid_injective LeftCancelMonoid.ext
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid toRightCancelMonoid	—	ext
toLeftCancelMonoid_injective 📖	mathematical	—	CancelMonoid LeftCancelMonoid toLeftCancelMonoid	—	—

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup	—	—	toGroup_injective Group.ext
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup	—	ext
toGroup_injective 📖	mathematical	—	CommGroup Group toGroup	—	—

CommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	—	toMonoid_injective Monoid.ext
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	ext
toMonoid_injective 📖	mathematical	—	CommMonoid Monoid toMonoid	—	—

DivInvMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid toInv	—	—	Monoid.ext MonoidHom.map_zpow' map_div' MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid toInv	—	ext

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid toDivInvMonoid	—	—	Monoid.ext toDivInvMonoid_injective DivInvMonoid.ext MonoidHom.map_inv
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid toDivInvMonoid	—	ext
toDivInvMonoid_injective 📖	mathematical	—	Group DivInvMonoid toDivInvMonoid	—	—

LeftCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	—	toMonoid_injective Monoid.ext
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	ext
toMonoid_injective 📖	mathematical	—	LeftCancelMonoid Monoid toMonoid	—	—

Monoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne toMulOneClass	—	—	MulOneClass.ext MonoidHom.map_pow
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne toMulOneClass	—	ext

RightCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	—	toMonoid_injective Monoid.ext
ext_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	ext
toMonoid_injective 📖	mathematical	—	RightCancelMonoid Monoid toMonoid	—	—

SubNegMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid toNeg	—	—	AddMonoid.ext AddMonoidHom.map_zsmul' map_sub' AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
ext_iff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid toNeg	—	ext

---

← Back to Index