Divisible

📁 Source: Mathlib/GroupTheory/Divisible.lean

Statistics

Metric	Count
Definitions divisibleByIntOfSMulTopEqTop, divisibleByIntOfDivisibleByNat, divisibleByNatOfDivisibleByInt, DivisibleBy, div, divisibleBy, rootableBy, rootableByIntOfRootableByNat, rootableByNatOfRootableByInt, divisibleBy, rootableBy, divisibleBy, rootableBy, divisibleBy, rootableBy, RootableBy, root, instDivisibleBy, instRootableBy, divisibleByIntOfCharZero, divisibleByOfSMulRightSurj, rootableByOfPowLeftSurj	22
Theorems smul_top_eq_top_of_divisibleBy_int, div_cancel, div_zero, surjective_smul, root_cancel, root_zero, surjective_pow, pow_left_surj_of_rootableBy, smul_right_surj_of_divisibleBy	9
Total	31

AddCommGroup

Definitions

Name	Category	Theorems
divisibleByIntOfSMulTopEqTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_top_eq_top_of_divisibleBy_int 📖	mathematical	—	AddSubgroup toAddGroup SemigroupAction.toSMul Monoid.toSemigroup Int.instMonoid MulAction.toSemigroupAction AddSubgroup.pointwiseMulAction Module.toDistribMulAction Int.instSemiring toAddCommMonoid toIntModule Top.top AddSubgroup.instTop	—	AddSubgroup.map_top_of_surjective DivisibleBy.div_cancel

AddGroup

Definitions

Name	Category	Theorems
divisibleByIntOfDivisibleByNat 📖	CompOp	—
divisibleByNatOfDivisibleByInt 📖	CompOp	—

DivisibleBy

Definitions

Name	Category	Theorems
div 📖	CompOp	2 math math: div_zero, div_cancel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_cancel 📖	mathematical	—	div	—	—
div_zero 📖	mathematical	—	div AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—
surjective_smul 📖	—	—	—	—	div_cancel

Function.Surjective

Definitions

Name	Category	Theorems
divisibleBy 📖	CompOp	—
rootableBy 📖	CompOp	—

Group

Definitions

Name	Category	Theorems
rootableByIntOfRootableByNat 📖	CompOp	—
rootableByNatOfRootableByInt 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
divisibleBy 📖	CompOp	—
rootableBy 📖	CompOp	—

Prod

Definitions

Name	Category	Theorems
divisibleBy 📖	CompOp	—
rootableBy 📖	CompOp	—

QuotientAddGroup

Definitions

Name	Category	Theorems
divisibleBy 📖	CompOp	—

QuotientGroup

Definitions

Name	Category	Theorems
rootableBy 📖	CompOp	—

RootableBy

Definitions

Name	Category	Theorems
root 📖	CompOp	2 math math: root_cancel, root_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
root_cancel 📖	mathematical	—	root	—	—
root_zero 📖	mathematical	—	root MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
surjective_pow 📖	—	—	—	—	root_cancel

ULift

Definitions

Name	Category	Theorems
instDivisibleBy 📖	CompOp	—
instRootableBy 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
DivisibleBy 📖	CompData	—
RootableBy 📖	CompData	—
divisibleByIntOfCharZero 📖	CompOp	—
divisibleByOfSMulRightSurj 📖	CompOp	—
rootableByOfPowLeftSurj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_left_surj_of_rootableBy 📖	—	—	—	—	RootableBy.root_cancel
smul_right_surj_of_divisibleBy 📖	—	—	—	—	DivisibleBy.div_cancel

---

← Back to Index