Basic

📁 Source: Mathlib/Algebra/Order/Module/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_smul, inf_eq_half_smul_add_sub_abs_sub, inf_eq_half_smul_add_sub_abs_sub', sup_eq_half_smul_add_add_abs_sub, sup_eq_half_smul_add_add_abs_sub'	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_smul 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	le_total abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono PosSMulMono.toSMulPosMono abs_of_nonpos IsOrderedRing.toIsOrderedAddMonoid smul_neg neg_smul neg_neg
inf_eq_half_smul_add_sub_abs_sub 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup abs	—	Nat.instAtLeastTwoHAddOfNat two_nsmul_inf_eq_add_sub_abs_sub IsOrderedAddMonoid.toAddLeftMono two_smul smul_smul invOf_mul_self one_smul
inf_eq_half_smul_add_sub_abs_sub' 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup abs	—	Nat.instAtLeastTwoHAddOfNat two_ne_zero' inf_eq_half_smul_add_sub_abs_sub
sup_eq_half_smul_add_add_abs_sub 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup abs SubNegMonoid.toSub	—	Nat.instAtLeastTwoHAddOfNat two_nsmul_sup_eq_add_add_abs_sub IsOrderedAddMonoid.toAddLeftMono two_smul smul_smul invOf_mul_self one_smul
sup_eq_half_smul_add_add_abs_sub' 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup abs SubNegMonoid.toSub	—	Nat.instAtLeastTwoHAddOfNat two_ne_zero' sup_eq_half_smul_add_add_abs_sub

---

← Back to Index