Slope

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Slope.lean

Statistics

Metric	Count
Definitions slope	1
Theorems slope_comp, slope_nonpos, slope_comp, slope_nonneg, slope_neg, slope_pos, eq_of_slope_eq_zero, lineMap_slope_lineMap_slope_lineMap, lineMap_slope_slope_sub_div_sub, slope_comm, slope_def_field, slope_def_module, slope_eq_zero_iff, slope_fun_def, slope_fun_def_field, slope_neg, slope_neg_fun, slope_neg_iff_of_le, slope_nonneg_iff_of_le, slope_nonpos_iff_of_le, slope_pos_iff_of_le, slope_same, slope_sub_smul, slope_vadd_const, sub_div_sub_smul_slope_add_sub_div_sub_smul_slope, sub_smul_slope, sub_smul_slope_vadd	27
Total	28

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slope_comp 📖	mathematical	—	slope DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing instFunLike LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear	—	LinearMap.map_smul linearMap_vsub

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slope_nonpos 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	Preorder.toLE slope addGroupIsAddTorsor AddCommGroup.toAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	slope_neg IsOrderedAddMonoid.toAddLeftMono MonotoneOn.slope_nonneg neg covariant_swap_add_of_covariant_add

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slope_comp 📖	mathematical	—	slope addGroupIsAddTorsor AddCommGroup.toAddGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	AffineMap.slope_comp

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slope_nonneg 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	Preorder.toLE NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid slope addGroupIsAddTorsor AddCommGroup.toAddGroup	—	le_total slope_nonneg_iff_of_le slope_comm

StrictAntiOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slope_neg 📖	mathematical	StrictAntiOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	Preorder.toLT slope addGroupIsAddTorsor AddCommGroup.toAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	slope_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono StrictMonoOn.slope_pos neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slope_pos 📖	mathematical	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid slope addGroupIsAddTorsor AddCommGroup.toAddGroup	—	lt_or_gt_of_ne slope_pos_iff_of_le LT.lt.le slope_comm

(root)

Definitions

Name	Category	Theorems
slope 📖	CompOp	120 math math: MonotoneOn.intervalIntegral_slope_le, ConvexOn.le_slope_of_hasDerivAt, StrictConvexOn.slope_lt_leftDeriv, ConvexOn.rightDeriv_le_slope_of_mem_interior, ConvexOn.monotoneOn_slope_lt, HasDerivWithinAt.liminf_right_slope_le, StrictConvexOn.deriv_lt_slope, StrictConcaveOn.lt_slope_of_hasDerivAt, StrictConcaveOn.slope_lt_rightDeriv, StrictConvexOn.rightDeriv_lt_slope, MonotoneOn.slope_nonneg, lineMap_le_map_iff_slope_le_slope_right, AffineMap.slope_comp, StrictConcaveOn.slope_lt_derivWithin, exists_dist_slope_lt_pairwiseDisjoint_hasSum, slope_pos_iff_of_le, ConcaveOn.slope_le_of_hasDerivAt, dslope_eventuallyEq_slope_nhdsNE, StrictConvexOn.lt_slope_of_hasDerivAt, StrictConcaveOn.deriv_lt_slope, StrictConcaveOn.slope_lt_deriv, ConvexOn.slope_le_deriv, ConcaveOn.antitoneOn_slope_gt, map_lt_lineMap_iff_slope_lt_slope_right, StrictConcaveOn.lt_slope_of_hasDerivWithinAt_Iio, StrictConvexOn.slope_lt_deriv, hasDerivAtFilter_iff_tendsto_slope, hasDerivAt_iff_tendsto_slope_left_right, bddAbove_slope_gt_of_mem_interior, sub_smul_slope_vadd, ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi, ConcaveOn.slope_anti, slope_neg_fun, slope_eq_zero_iff, MonotoneOn.intervalIntegrable_slope, ConvexOn.slope_le_leftDeriv, ConcaveOn.antitoneOn_slope_lt, slope_comm, ConvexOn.le_slope_of_hasDerivWithinAt_Ioi, map_lt_lineMap_iff_slope_lt_slope_left, StrictConcaveOn.slope_lt_of_hasDerivAt, eqOn_dslope_slope, slope_pos_iff, map_le_lineMap_iff_slope_le_slope_right, StrictConcaveOn.derivWithin_lt_slope, StrictConvexOn.slope_lt_derivWithin, ConvexOn.slope_le_of_hasDerivWithinAt, AntitoneOn.slope_nonpos, StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio, ConvexOn.slope_mono, ConcaveOn.le_slope_of_hasDerivWithinAt, dslope_of_ne, slope_def_field, slope_fun_def, LinearMap.slope_comp, ConcaveOn.slope_le_derivWithin, lineMap_lt_map_iff_slope_lt_slope, slope_neg, dslope_eventuallyEq_slope_of_ne, ConcaveOn.leftDeriv_le_slope, ConcaveOn.derivWithin_le_slope, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior, bddBelow_slope_lt_of_mem_interior, ConcaveOn.deriv_le_slope, HasDerivAt.tendsto_slope, lineMap_le_map_iff_slope_le_slope, ConcaveOn.slope_le_of_hasDerivWithinAt, slope_pos_iff_gt, ConcaveOn.le_slope_of_hasDerivWithinAt_Iio, StrictConvexOn.lt_slope_of_hasDerivWithinAt, HasDerivWithinAt.limsup_slope_le', StrictConcaveOn.slope_lt_of_hasDerivWithinAt, ConvexOn.derivWithin_le_slope, ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior, lineMap_lt_map_iff_slope_lt_slope_left, StrictConcaveOn.slope_lt_of_hasDerivWithinAt_Ioi, slope_vadd_const, IntervalIntegrable.intervalIntegrable_slope, StrictAntiOn.slope_neg, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior, map_le_lineMap_iff_slope_le_slope, exists_deriv_eq_slope', StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi, slope_nonpos_iff_of_le, ConvexOn.slope_le_of_hasDerivAt, slope_sub_smul, ConvexOn.deriv_le_slope, ConvexOn.rightDeriv_le_slope, sub_smul_slope, StrictConcaveOn.lt_slope_of_hasDerivWithinAt, StrictConvexOn.derivWithin_lt_slope, StrictConvexOn.slope_lt_of_hasDerivWithinAt, ConcaveOn.slope_le_rightDeriv, ConvexOn.monotoneOn_slope_gt, ConvexOn.le_slope_of_hasDerivWithinAt, ConvexOn.slope_le_derivWithin, slope_neg_iff_of_le, slope_fun_def_field, map_le_lineMap_iff_slope_le_slope_left, map_lt_lineMap_iff_slope_lt_slope, slope_nonneg_iff_of_le, hasDerivAt_iff_tendsto_slope, lineMap_le_map_iff_slope_le_slope_left, lineMap_slope_lineMap_slope_lineMap, StrictConcaveOn.leftDeriv_lt_slope, hasDerivWithinAt_iff_tendsto_slope', lineMap_slope_slope_sub_div_sub, StrictMonoOn.slope_pos, hasDerivWithinAt_iff_tendsto_slope, ConcaveOn.slope_le_deriv, ConvexOn.slope_le_of_hasDerivWithinAt_Iio, lineMap_lt_map_iff_slope_lt_slope_right, ConcaveOn.le_slope_of_hasDerivAt, slope_def_module, slope_same, ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior, sub_div_sub_smul_slope_add_sub_div_sub_smul_slope, ConvexOn.slope_le_leftDeriv_of_mem_interior, HasDerivWithinAt.limsup_slope_le, StrictConvexOn.slope_lt_of_hasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_slope_eq_zero 📖	—	slope NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	sub_smul_slope_vadd smul_zero zero_vadd
lineMap_slope_lineMap_slope_lineMap 📖	mathematical	—	DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope	—	AffineMap.lineMap_same slope_same slope_comm AffineMap.lineMap_apply_ring eq_div_iff sub_ne_zero sub_mul one_mul mul_sub sub_sub sub_sub_cancel lineMap_slope_slope_sub_div_sub
lineMap_slope_slope_sub_div_sub 📖	mathematical	—	DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap slope DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	AffineMap.lineMap_apply_module sub_div_sub_smul_slope_add_sub_div_sub_smul_slope AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg sub_ne_zero one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
slope_comm 📖	mathematical	—	slope	—	slope.eq_1 neg_vsub_eq_vsub_rev smul_neg neg_smul neg_inv neg_sub
slope_def_field 📖	mathematical	—	slope Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	div_eq_inv_mul
slope_def_module 📖	mathematical	—	slope addGroupIsAddTorsor AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	—
slope_eq_zero_iff 📖	mathematical	—	slope addGroupIsAddTorsor AddCommGroup.toAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Field.isDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero
slope_fun_def 📖	mathematical	—	slope SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing VSub.vsub AddTorsor.toVSub	—	—
slope_fun_def_field 📖	mathematical	—	slope Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	div_eq_inv_mul
slope_neg 📖	mathematical	—	slope addGroupIsAddTorsor AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_sub_neg neg_sub
slope_neg_fun 📖	mathematical	—	slope addGroupIsAddTorsor AddCommGroup.toAddGroup Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	slope_neg
slope_neg_iff_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT slope addGroupIsAddTorsor AddCommGroup.toAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	slope_neg_fun IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add slope_pos_iff_of_le
slope_nonneg_iff_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid slope addGroupIsAddTorsor AddCommGroup.toAddGroup	—	slope_same smul_nonneg sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing vsub_eq_sub one_smul mul_inv_cancel₀ sub_eq_zero SemigroupAction.mul_smul slope.eq_1 inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
slope_nonpos_iff_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	slope addGroupIsAddTorsor AddCommGroup.toAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	slope_neg_fun IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add slope_nonneg_iff_of_le
slope_pos_iff_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid slope addGroupIsAddTorsor AddCommGroup.toAddGroup	—	slope_nonneg_iff_of_le
slope_same 📖	mathematical	—	slope NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	slope.eq_1 sub_self inv_zero zero_smul
slope_sub_smul 📖	mathematical	—	slope addGroupIsAddTorsor AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	sub_self zero_smul sub_zero inv_smul_smul₀ sub_ne_zero
slope_vadd_const 📖	mathematical	—	slope HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor	—	vadd_vsub_vadd_cancel_right
sub_div_sub_smul_slope_add_sub_div_sub_smul_slope 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing slope	—	sub_self zero_div zero_smul zero_add div_zero slope_same smul_zero div_self sub_ne_zero one_smul add_zero add_comm div_eq_inv_mul SemigroupAction.mul_smul smul_inv_smul₀ vsub_add_vsub_cancel
sub_smul_slope 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing slope VSub.vsub AddTorsor.toVSub	—	eq_or_ne sub_self zero_smul vsub_self slope.eq_1 smul_inv_smul₀ sub_ne_zero
sub_smul_slope_vadd 📖	mathematical	—	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing slope	—	sub_smul_slope vsub_vadd

---

← Back to Index