Quotient

📁 Source: Mathlib/Algebra/CharZero/Quotient.lean

Statistics

Metric	Count
Definitions	0
Theorems nsmul_mem_zmultiples_iff_exists_sub_div, zsmul_mem_zmultiples_iff_exists_sub_div, zmultiples_nsmul_eq_nsmul_iff, zmultiples_zsmul_eq_zsmul_iff	4
Total	4

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nsmul_mem_zmultiples_iff_exists_sub_div 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing SetLike.instMembership instSetLike zmultiples AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast	—	natCast_zsmul zsmul_mem_zmultiples_iff_exists_sub_div Int.cast_natCast
zsmul_mem_zmultiples_iff_exists_sub_div 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing SetLike.instMembership instSetLike zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid SubNegMonoid.toSub AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddGroupWithOne.toIntCast	—	mem_zmultiples_iff div_eq_mul_inv AddCommMonoid.nat_isScalarTower Int.cast_ne_zero mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero DivisionRing.isDomain smul_add AddGroup.int_smulCommClass zsmul_eq_mul mul_inv_cancel₀ mul_one smul_smul LT.lt.trans_eq Int.emod_lt_abs Int.abs_eq_natAbs

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zmultiples_nsmul_eq_nsmul_iff 📖	mathematical	—	HasQuotient.Quotient AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing instHasQuotientAddSubgroup AddSubgroup.zmultiples AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_of_comm Ring.toAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Quotient.addCommGroup DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	AddSubgroup.normal_of_comm natCast_zsmul zmultiples_zsmul_eq_zsmul_iff Int.cast_natCast
zmultiples_zsmul_eq_zsmul_iff 📖	mathematical	—	HasQuotient.Quotient AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_of_comm Ring.toAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Quotient.addCommGroup AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddGroupWithOne.toIntCast	—	AddSubgroup.normal_of_comm AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div

---

← Back to Index