DivisibleHull

📁 Source: Mathlib/GroupTheory/DivisibleHull.lean

Statistics

Metric	Count
Definitions DivisibleHull, archimedeanClassOrderIso, coeAddMonoidHom, coeOrderAddMonoidHom, instCoe, instLE, instLinearOrder, instModuleNNRat, instModuleRat, instSMulRat, liftOn, liftOn₂, mk	13
Theorems archimedeanClassMk_mk_eq, archimedeanClassOrderIso_apply, archimedeanClassOrderIso_symm_apply, coeAddMonoidHom_apply, coeOrderAddMonoidHom_apply, coe_add, coe_inj, coe_injective, ind, instIsOrderedCancelAddMonoid, instIsStrictOrderedModuleNNRat, instIsStrictOrderedModuleRat, liftOn_mk, liftOn₂_mk, mk_add_mk, mk_add_mk_left, mk_eq_mk, mk_eq_mk_iff_smul_eq_smul, mk_le_mk, mk_left_injective, mk_lt_mk, mk_zero, neg_mk, nnqsmul_mk, nsmul_mk, qsmul_def, qsmul_mk, qsmul_of_nonneg, qsmul_of_nonpos, zero_qsmul, zsmul_mk	31
Total	44

DivisibleHull

Definitions

Name	Category	Theorems
archimedeanClassOrderIso 📖	CompOp	2 math math: archimedeanClassOrderIso_apply, archimedeanClassOrderIso_symm_apply
coeAddMonoidHom 📖	CompOp	1 math math: coeAddMonoidHom_apply
coeOrderAddMonoidHom 📖	CompOp	2 math math: coeOrderAddMonoidHom_apply, archimedeanClassOrderIso_apply
instCoe 📖	CompOp	—
instLE 📖	CompOp	1 math math: mk_le_mk
instLinearOrder 📖	CompOp	8 math math: archimedeanClassMk_mk_eq, instIsStrictOrderedModuleNNRat, instIsOrderedCancelAddMonoid, coeOrderAddMonoidHom_apply, archimedeanClassOrderIso_apply, mk_lt_mk, archimedeanClassOrderIso_symm_apply, instIsStrictOrderedModuleRat
instModuleNNRat 📖	CompOp	5 math math: instIsStrictOrderedModuleNNRat, qsmul_def, qsmul_of_nonneg, qsmul_of_nonpos, nnqsmul_mk
instModuleRat 📖	CompOp	—
instSMulRat 📖	CompOp	6 math math: qsmul_def, qsmul_of_nonneg, qsmul_mk, qsmul_of_nonpos, instIsStrictOrderedModuleRat, zero_qsmul
liftOn 📖	CompOp	1 math math: liftOn_mk
liftOn₂ 📖	CompOp	1 math math: liftOn₂_mk
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
archimedeanClassMk_mk_eq 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid OreLocalization.instAddCommGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction AddCommMonoid.toNatModule instLinearOrder IsOrderedAddMonoid.toIsOrderedCancelAddMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid	—	instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add natCast_zsmul smul_smul mul_comm IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid ArchimedeanClass.mk_smul IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing instArchimedeanInt PosSMulStrictMono.toPosSMulMono instPosSMulStrictMonoIntOfIsOrderedAddMonoid
archimedeanClassOrderIso_apply 📖	mathematical	—	DFunLike.coe OrderIso ArchimedeanClass DivisibleHull AddCommGroup.toAddCommMonoid OreLocalization.instAddCommGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction AddCommMonoid.toNatModule instLinearOrder IsOrderedAddMonoid.toIsOrderedCancelAddMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder instFunLikeOrderIso archimedeanClassOrderIso OrderHom OrderHom.instFunLike ArchimedeanClass.orderHom coeOrderAddMonoidHom	—	IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid
archimedeanClassOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso ArchimedeanClass DivisibleHull AddCommGroup.toAddCommMonoid OreLocalization.instAddCommGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction AddCommMonoid.toNatModule instLinearOrder IsOrderedAddMonoid.toIsOrderedCancelAddMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder instFunLikeOrderIso OrderIso.symm archimedeanClassOrderIso	—	IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid
coeAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom DivisibleHull AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid OreLocalization.instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction AddCommMonoid.toNatModule AddMonoidHom.instFunLike coeAddMonoidHom coe	—	—
coeOrderAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe OrderAddMonoidHom DivisibleHull AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder IsOrderedAddMonoid.toIsOrderedCancelAddMonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup OreLocalization.instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule OrderAddMonoidHom.instFunLike coeOrderAddMonoidHom coe	—	IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
coe_add 📖	mathematical	—	coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DivisibleHull OreLocalization.instAdd MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule	—	mk_add_mk_left
coe_inj 📖	mathematical	—	coe	—	coe_injective
coe_injective 📖	mathematical	—	DivisibleHull coe	—	mk_left_injective
ind 📖	—	—	—	—	LocalizedModule.induction_on
instIsOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid DivisibleHull OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction AddCommMonoid.toNatModule SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	IsOrderedCancelAddMonoid.of_add_lt_add_left ind SemigroupAction.mul_smul smul_add smul_smul add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid nsmul_lt_nsmul_right IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add PNat.ne_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw
instIsStrictOrderedModuleNNRat 📖	mathematical	—	IsStrictOrderedModule NNRat DivisibleHull SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass OreLocalization.instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield OreLocalization.instAddCommMonoidOreLocalization instModuleNNRat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring OreLocalization.instZero DistribMulAction.toMulAction	—	ind NNRat.den_pos smul_smul mul_right_comm SemigroupAction.mul_smul StrictMono.lt_iff_lt nsmul_right_strictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd LT.lt.ne smul_lt_smul_of_pos_right instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono NNRat.lt_def nsmul_zero one_smul mk_zero
instIsStrictOrderedModuleRat 📖	mathematical	—	IsStrictOrderedModule DivisibleHull AddCommGroup.toAddCommMonoid instSMulRat Rat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder IsOrderedAddMonoid.toIsOrderedCancelAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing OreLocalization.instZero MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule	—	IsOrderedAddMonoid.toIsOrderedCancelAddMonoid LT.lt.le qsmul_of_nonneg smul_lt_smul_of_pos_left IsStrictOrderedModule.toPosSMulStrictMono instIsStrictOrderedModuleNNRat lt_of_sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid sub_smul sub_pos_of_lt Rat.instAddLeftMono smul_pos Rat.cast_sub Rat.instCharZero
liftOn_mk 📖	mathematical	—	liftOn	—	—
liftOn₂_mk 📖	mathematical	—	liftOn₂	—	—
mk_add_mk 📖	mathematical	—	DivisibleHull OreLocalization.instAdd MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul PNat.val PNat instMulPNat	—	—
mk_add_mk_left 📖	mathematical	—	DivisibleHull OreLocalization.instAdd MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smul_add smul_smul one_mul
mk_eq_mk 📖	mathematical	—	AddMonoid.toNatSMul AddCommMonoid.toAddMonoid PNat.val	—	LocalizedModule.mk_eq Equiv.exists_congr_left
mk_eq_mk_iff_smul_eq_smul 📖	mathematical	—	AddMonoid.toNatSMul AddCommMonoid.toAddMonoid PNat.val	—	IsAddTorsionFree.to_isTorsionFree_nat Nat.instIsCancelMulZero
mk_le_mk 📖	mathematical	—	DivisibleHull instLE Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNatSMul AddCommMonoid.toAddMonoid PNat.val	—	—
mk_left_injective 📖	mathematical	—	DivisibleHull	—	nsmul_right_injective
mk_lt_mk 📖	mathematical	—	DivisibleHull Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder AddMonoid.toNatSMul AddCommMonoid.toAddMonoid PNat.val	—	—
mk_zero 📖	mathematical	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DivisibleHull OreLocalization.instZero MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction Module.toDistribMulAction AddCommMonoid.toNatModule	—	OreLocalization.zero_oreDiv
neg_mk 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid OreLocalization.instNegOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommGroup.toAddGroup Module.toDistribMulAction AddCommMonoid.toNatModule NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	eq_neg_of_add_eq_zero_left mk_add_mk_left neg_add_cancel mk_zero
nnqsmul_mk 📖	mathematical	—	NNRat DivisibleHull SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass OreLocalization.instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield OreLocalization.instAddCommMonoidOreLocalization instModuleNNRat AddMonoid.toNatSMul NNRat.num PNat instMulPNat NNRat.den NNRat.den_pos	—	NNRat.den_pos NNRat.isFractionRing IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instNontrivial eq_natCast RingHom.instRingHomClass NNRat.mul_den_eq_num
nsmul_mk 📖	mathematical	—	DivisibleHull AddMonoid.toNatSMul OreLocalization.instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule	—	zero_nsmul mk_zero add_nsmul one_smul mk_add_mk_left
qsmul_def 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid instSMulRat SubNegMonoid.toZSMul AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommGroup.toAddGroup Module.toDistribMulAction AddCommMonoid.toNatModule SignType.cast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DFunLike.coe OrderHom SignType Rat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Rat.commRing NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass OreLocalization.instAddMonoid AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield OreLocalization.instAddCommMonoidOreLocalization instModuleNNRat	—	—
qsmul_mk 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid instSMulRat SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PNat instMulPNat	—	le_total qsmul_of_nonneg NNRat.den_pos natCast_zsmul Nat.cast_natAbs Int.cast_abs Int.instIsStrictOrderedRing Int.instIsOrderedAddMonoid Left.nonneg_neg_iff Rat.instAddLeftMono qsmul_of_nonpos neg_smul neg_neg
qsmul_of_nonneg 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid instSMulRat NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass OreLocalization.instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield OreLocalization.instAddCommMonoidOreLocalization instModuleNNRat	—	LE.le.eq_or_lt abs_nonneg Rat.instAddLeftMono covariant_swap_add_of_covariant_add sign_zero abs_zero zero_smul smul_zero abs_of_pos sign_pos one_smul
qsmul_of_nonpos 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid instSMulRat OreLocalization.instNegOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommGroup.toAddGroup Module.toDistribMulAction AddCommMonoid.toNatModule NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass OreLocalization.instAddMonoid AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield OreLocalization.instAddCommMonoidOreLocalization instModuleNNRat	—	LE.le.eq_or_lt Left.nonneg_neg_iff Rat.instAddLeftMono abs_nonneg covariant_swap_add_of_covariant_add sign_zero abs_zero zero_smul smul_zero neg_zero abs_of_neg sign_neg SignType.coe_neg neg_smul one_smul
zero_qsmul 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid instSMulRat OreLocalization.instZero MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AddCommMonoid.toNatModule	—	abs_nonneg Rat.instAddLeftMono covariant_swap_add_of_covariant_add sign_zero abs_zero zero_smul smul_zero
zsmul_mk 📖	mathematical	—	DivisibleHull AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.instCommSemiring nonZeroDivisors Nat.instMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommGroup.toAddGroup Module.toDistribMulAction AddCommMonoid.toNatModule	—	Int.cast_smul_eq_zsmul one_mul

(root)

Definitions

Name	Category	Theorems
DivisibleHull 📖	CompOp	25 math math: DivisibleHull.archimedeanClassMk_mk_eq, DivisibleHull.mk_add_mk_left, DivisibleHull.instIsStrictOrderedModuleNNRat, DivisibleHull.mk_le_mk, DivisibleHull.coeAddMonoidHom_apply, DivisibleHull.instIsOrderedCancelAddMonoid, DivisibleHull.mk_left_injective, DivisibleHull.qsmul_def, DivisibleHull.qsmul_of_nonneg, DivisibleHull.coeOrderAddMonoidHom_apply, DivisibleHull.nsmul_mk, DivisibleHull.coe_injective, DivisibleHull.mk_add_mk, DivisibleHull.qsmul_mk, DivisibleHull.archimedeanClassOrderIso_apply, DivisibleHull.mk_lt_mk, DivisibleHull.zsmul_mk, DivisibleHull.neg_mk, DivisibleHull.qsmul_of_nonpos, DivisibleHull.archimedeanClassOrderIso_symm_apply, DivisibleHull.instIsStrictOrderedModuleRat, DivisibleHull.coe_add, DivisibleHull.mk_zero, DivisibleHull.zero_qsmul, DivisibleHull.nnqsmul_mk

---

← Back to Index