Div

📁 Source: Mathlib/Algebra/Order/Floor/Div.lean

Statistics

Metric	Count
Definitions CeilDiv, ceilDiv, instCeilDiv, instFloorDiv, FloorDiv, floorDiv, instCeilDiv, instFloorDiv, instCeilDiv, instFloorDiv, «term_⌈/⌉_», «term_⌊/⌋_»	12
Theorems ceilDiv_gc, ceilDiv_nonpos, zero_ceilDiv, ceilDiv_apply, ceilDiv_def, coe_ceilDiv_def, coe_floorDiv, floorDiv_apply, floorDiv_def, support_ceilDiv_subset, support_floorDiv_subset, floorDiv_gc, floorDiv_nonpos, zero_floorDiv, ceilDiv_eq_add_pred_div, floorDiv_eq_div, ceilDiv_apply, ceilDiv_def, floorDiv_apply, floorDiv_def, ceilDiv_le_iff_le_mul, ceilDiv_le_iff_le_smul, ceilDiv_of_nonpos, ceilDiv_one, ceilDiv_zero, floorDiv_le_ceilDiv, floorDiv_of_nonpos, floorDiv_one, floorDiv_zero, gc_floorDiv_mul, gc_floorDiv_smul, gc_mul_ceilDiv, gc_smul_ceilDiv, le_floorDiv_iff_mul_le, le_floorDiv_iff_smul_le, le_smul_ceilDiv, smul_ceilDiv, smul_floorDiv, smul_floorDiv_le, zero_ceilDiv, zero_floorDiv	41
Total	53

CeilDiv

Definitions

Name	Category	Theorems
ceilDiv 📖	CompOp	23 math math: ceilDiv_le_iff_le_smul, Pi.ceilDiv_def, Finsupp.coe_ceilDiv_def, ceilDiv_nonpos, Finsupp.ceilDiv_apply, Finsupp.ceilDiv_def, Nat.ceilRoot_def, Finsupp.support_ceilDiv_subset, gc_mul_ceilDiv, Nat.factorization_ceilRoot, floorDiv_le_ceilDiv, ceilDiv_gc, smul_ceilDiv, ceilDiv_one, ceilDiv_of_nonpos, zero_ceilDiv, zero_ceilDiv, gc_smul_ceilDiv, ceilDiv_zero, ceilDiv_le_iff_le_mul, Nat.ceilDiv_eq_add_pred_div, Pi.ceilDiv_apply, le_smul_ceilDiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceilDiv_gc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	GaloisConnection ceilDiv SMulZeroClass.toSMul	—	—
ceilDiv_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	ceilDiv	—	—
zero_ceilDiv 📖	mathematical	—	ceilDiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—

Finsupp

Definitions

Name	Category	Theorems
instCeilDiv 📖	CompOp	6 math math: coe_ceilDiv_def, ceilDiv_apply, ceilDiv_def, Nat.ceilRoot_def, support_ceilDiv_subset, Nat.factorization_ceilRoot
instFloorDiv 📖	CompOp	6 math math: floorDiv_def, floorDiv_apply, support_floorDiv_subset, Nat.factorization_floorRoot, coe_floorDiv, Nat.floorRoot_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceilDiv_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike CeilDiv.ceilDiv instAddCommMonoid partialorder smulZeroClass instCeilDiv	—	—
ceilDiv_def 📖	mathematical	—	CeilDiv.ceilDiv Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid partialorder smulZeroClass instCeilDiv mapRange zero_ceilDiv	—	—
coe_ceilDiv_def 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike CeilDiv.ceilDiv instAddCommMonoid partialorder smulZeroClass instCeilDiv	—	—
coe_floorDiv 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike FloorDiv.floorDiv instAddCommMonoid partialorder smulZeroClass instFloorDiv	—	—
floorDiv_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike FloorDiv.floorDiv instAddCommMonoid partialorder smulZeroClass instFloorDiv	—	—
floorDiv_def 📖	mathematical	—	FloorDiv.floorDiv Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid partialorder smulZeroClass instFloorDiv mapRange zero_floorDiv	—	—
support_ceilDiv_subset 📖	mathematical	—	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CeilDiv.ceilDiv Finsupp instAddCommMonoid partialorder smulZeroClass instCeilDiv	—	zero_ceilDiv
support_floorDiv_subset 📖	mathematical	—	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid FloorDiv.floorDiv Finsupp instAddCommMonoid partialorder smulZeroClass instFloorDiv	—	zero_floorDiv

FloorDiv

Definitions

Name	Category	Theorems
floorDiv 📖	CompOp	23 math math: floorDiv_nonpos, Nat.floorDiv_eq_div, floorDiv_of_nonpos, Finsupp.floorDiv_def, floorDiv_gc, zero_floorDiv, gc_floorDiv_mul, Finsupp.floorDiv_apply, floorDiv_zero, Pi.floorDiv_def, smul_floorDiv_le, floorDiv_le_ceilDiv, Finsupp.support_floorDiv_subset, smul_floorDiv, floorDiv_one, le_floorDiv_iff_mul_le, Nat.factorization_floorRoot, Finsupp.coe_floorDiv, Nat.floorRoot_def, zero_floorDiv, gc_floorDiv_smul, le_floorDiv_iff_smul_le, Pi.floorDiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
floorDiv_gc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	GaloisConnection SMulZeroClass.toSMul floorDiv	—	—
floorDiv_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	floorDiv	—	—
zero_floorDiv 📖	mathematical	—	floorDiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—

Nat

Definitions

Name	Category	Theorems
instCeilDiv 📖	CompOp	3 math math: ceilRoot_def, factorization_ceilRoot, ceilDiv_eq_add_pred_div
instFloorDiv 📖	CompOp	3 math math: floorDiv_eq_div, factorization_floorRoot, floorRoot_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceilDiv_eq_add_pred_div 📖	mathematical	—	CeilDiv.ceilDiv instAddCommMonoid instPartialOrder DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass instAddMonoid instDistribSMul instNonUnitalNonAssocSemiring instCeilDiv	—	—
floorDiv_eq_div 📖	mathematical	—	FloorDiv.floorDiv instAddCommMonoid instPartialOrder DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass instAddMonoid instDistribSMul instNonUnitalNonAssocSemiring instFloorDiv	—	—

Pi

Definitions

Name	Category	Theorems
instCeilDiv 📖	CompOp	2 math math: ceilDiv_def, ceilDiv_apply
instFloorDiv 📖	CompOp	2 math math: floorDiv_def, floorDiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceilDiv_apply 📖	mathematical	—	CeilDiv.ceilDiv addCommMonoid partialOrder smulZeroClass AddZero.toZero AddZeroClass.toAddZero instCeilDiv	—	—
ceilDiv_def 📖	mathematical	—	CeilDiv.ceilDiv addCommMonoid partialOrder smulZeroClass AddZero.toZero AddZeroClass.toAddZero instCeilDiv	—	—
floorDiv_apply 📖	mathematical	—	FloorDiv.floorDiv addCommMonoid partialOrder smulZeroClass AddZero.toZero AddZeroClass.toAddZero instFloorDiv	—	—
floorDiv_def 📖	mathematical	—	FloorDiv.floorDiv addCommMonoid partialOrder smulZeroClass AddZero.toZero AddZeroClass.toAddZero instFloorDiv	—	—

(root)

Definitions

Name	Category	Theorems
CeilDiv 📖	CompData	—
FloorDiv 📖	CompData	—
«term_⌈/⌉_» 📖	CompOp	—
«term_⌊/⌋_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceilDiv_le_iff_le_mul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE CeilDiv.ceilDiv NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ceilDiv_le_iff_le_smul
ceilDiv_le_iff_le_smul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE CeilDiv.ceilDiv SMulZeroClass.toSMul	—	gc_smul_ceilDiv
ceilDiv_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	CeilDiv.ceilDiv	—	CeilDiv.ceilDiv_nonpos
ceilDiv_one 📖	mathematical	—	CeilDiv.ceilDiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulActionWithZero.toSMulWithZero AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eq_of_forall_ge_iff zero_lt_one' IsOrderedRing.toZeroLEOneClass NeZero.one one_smul
ceilDiv_zero 📖	mathematical	—	CeilDiv.ceilDiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	ceilDiv_of_nonpos
floorDiv_le_ceilDiv 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder FloorDiv.floorDiv SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder CeilDiv.ceilDiv	—	le_or_gt floorDiv_of_nonpos ceilDiv_of_nonpos le_of_smul_le_smul_left LE.le.trans smul_floorDiv_le le_smul_ceilDiv
floorDiv_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	FloorDiv.floorDiv	—	FloorDiv.floorDiv_nonpos
floorDiv_one 📖	mathematical	—	FloorDiv.floorDiv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulActionWithZero.toSMulWithZero AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eq_of_forall_le_iff zero_lt_one' IsOrderedRing.toZeroLEOneClass NeZero.one one_smul
floorDiv_zero 📖	mathematical	—	FloorDiv.floorDiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	floorDiv_of_nonpos
gc_floorDiv_mul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	GaloisConnection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib FloorDiv.floorDiv NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul	—	gc_floorDiv_smul
gc_floorDiv_smul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	GaloisConnection SMulZeroClass.toSMul FloorDiv.floorDiv	—	FloorDiv.floorDiv_gc
gc_mul_ceilDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	GaloisConnection CeilDiv.ceilDiv NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	gc_smul_ceilDiv
gc_smul_ceilDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	GaloisConnection CeilDiv.ceilDiv SMulZeroClass.toSMul	—	CeilDiv.ceilDiv_gc
le_floorDiv_iff_mul_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE FloorDiv.floorDiv NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero	—	le_floorDiv_iff_smul_le
le_floorDiv_iff_smul_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE FloorDiv.floorDiv SMulZeroClass.toSMul	—	gc_floorDiv_smul
le_smul_ceilDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE SMulZeroClass.toSMul CeilDiv.ceilDiv	—	ceilDiv_le_iff_le_smul le_rfl
smul_ceilDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	CeilDiv.ceilDiv NonUnitalNonAssocSemiring.toAddCommMonoid SMulWithZero.toSMulZeroClass MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulActionWithZero.toSMulWithZero SMulZeroClass.toSMul	—	eq_of_forall_ge_iff
smul_floorDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	FloorDiv.floorDiv NonUnitalNonAssocSemiring.toAddCommMonoid SMulWithZero.toSMulZeroClass MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulActionWithZero.toSMulWithZero SMulZeroClass.toSMul	—	eq_of_forall_le_iff
smul_floorDiv_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE SMulZeroClass.toSMul FloorDiv.floorDiv	—	le_floorDiv_iff_smul_le le_rfl
zero_ceilDiv 📖	mathematical	—	CeilDiv.ceilDiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	CeilDiv.zero_ceilDiv
zero_floorDiv 📖	mathematical	—	FloorDiv.floorDiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	FloorDiv.zero_floorDiv

---

← Back to Index