Ray

📁 Source: Mathlib/LinearAlgebra/Ray.lean

Statistics

Metric	Count
Definitions `instInvolutiveNeg`, `map`, `someRayVector`, `someVector`, `RayVector`, `Setoid`, `instInvolutiveNeg`, `instNeg`, `mapLinearEquiv`, `SameRay`, `instMulActionRay`, `instMulActionRayVector`, `instNegRay`, `rayOfNeZero`	14
Theorems `sameRay_map_iff`, `ind`, `linearEquiv_smul_eq_map`, `map_apply`, `map_neg`, `map_refl`, `map_symm`, `ne_neg_self`, `neg_units_smul`, `someRayVector_ray`, `someVector_ne_zero`, `someVector_ray`, `units_smul_of_neg`, `units_smul_of_pos`, `coe_neg`, `equiv_neg_iff`, `add_left`, `add_right`, `exists_eq_smul`, `exists_eq_smul_add`, `exists_nonneg_left`, `exists_nonneg_right`, `exists_pos`, `exists_pos_left`, `exists_pos_right`, `map`, `neg`, `nonneg_smul_left`, `nonneg_smul_right`, `of_neg`, `of_subsingleton`, `of_subsingleton'`, `pos_smul_left`, `pos_smul_right`, `refl`, `rfl`, `sameRay_comm`, `sameRay_map_iff`, `sameRay_nonneg_smul_left`, `sameRay_nonneg_smul_right`, `sameRay_pos_smul_left`, `sameRay_pos_smul_right`, `smul`, `trans`, `zero_left`, `zero_right`, `eq_zero_of_sameRay_neg_smul_right`, `eq_zero_of_sameRay_self_neg`, `equiv_iff_sameRay`, `exists_nonneg_left_iff_sameRay`, `exists_nonneg_right_iff_sameRay`, `exists_pos_left_iff_sameRay`, `exists_pos_left_iff_sameRay_and_ne_zero`, `exists_pos_right_iff_sameRay`, `exists_pos_right_iff_sameRay_and_ne_zero`, `instNonemptyRayOfNontrivial`, `instNonemptyRayVectorOfNontrivial`, `neg_rayOfNeZero`, `ray_eq_iff`, `ray_pos_smul`, `sameRay_neg_iff`, `sameRay_neg_smul_left_iff`, `sameRay_neg_smul_left_iff_of_ne`, `sameRay_neg_smul_right_iff`, `sameRay_neg_smul_right_iff_of_ne`, `sameRay_neg_swap`, `sameRay_of_mem_orbit`, `sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent`, `sameRay_or_sameRay_neg_iff_not_linearIndependent`, `sameRay_smul_left_iff`, `sameRay_smul_left_iff_of_ne`, `sameRay_smul_right_iff`, `sameRay_smul_right_iff_of_ne`, `smul_rayOfNeZero`, `units_inv_smul`, `units_smul_eq_neg_iff`, `units_smul_eq_self_iff`	77
Total	91

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sameRay_map_iff` 📖	mathematical	`DFunLike.coe`	`SameRay`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`

Module.Ray

Definitions

Name	Category	Theorems
`instInvolutiveNeg` 📖	CompOp	—
`map` 📖	CompOp	5 math math: `map_symm`, `linearEquiv_smul_eq_map`, `map_refl`, `map_apply`, `map_neg`
`someRayVector` 📖	CompOp	1 math math: `someRayVector_ray`
`someVector` 📖	CompOp	1 math math: `someVector_ray`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ind` 📖	—	`rayOfNeZero`	—	—	—
`linearEquiv_smul_eq_map` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Ray` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `MulAction.toSemigroupAction` `instMulActionRay` `LinearEquiv.applyDistribMulAction` `LinearEquiv.apply_smulCommClass` `Algebra.toSMul` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `map`	—	`RingHomInvPair.ids` `LinearEquiv.apply_smulCommClass` `IsScalarTower.left`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Module.Ray` `EquivLike.toFunLike` `Equiv.instEquivLike` `map` `rayOfNeZero` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearEquiv.instEquivLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `LinearEquiv.map_ne_zero_iff`	—	`RingHomInvPair.ids`
`map_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Module.Ray` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `map` `instNegRay`	—	`RingHomInvPair.ids` `ind` `neg_ne_zero` `LinearEquiv.map_ne_zero_iff` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `rayOfNeZero.congr_simp`
`map_refl` 📖	mathematical	—	`map` `LinearEquiv.refl` `CommSemiring.toSemiring` `Equiv.refl` `Module.Ray`	—	`Equiv.ext` `ind`
`map_symm` 📖	mathematical	—	`Equiv.symm` `Module.Ray` `map` `LinearEquiv.symm` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids`
`ne_neg_self` 📖	—	—	—	—	`ind` `neg_ne_zero` `neg_rayOfNeZero` `ray_eq_iff` `eq_zero_of_sameRay_self_neg`
`neg_units_smul` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.Ray` `AddCommGroup.toAddCommMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `Units.instGroup` `Units.instDistribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.smulCommClass_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instNegRay`	—	`ind` `Units.smulCommClass_right` `smulCommClass_self` `neg_ne_zero` `smul_ne_zero_iff_ne` `neg_smul` `rayOfNeZero.congr_simp`
`someRayVector_ray` 📖	mathematical	—	`RayVector` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `RayVector.Setoid` `someRayVector`	—	`Quotient.out_eq`
`someVector_ne_zero` 📖	—	—	—	—	—
`someVector_ray` 📖	mathematical	—	`rayOfNeZero` `someVector` `someVector_ne_zero`	—	`someVector_ne_zero` `Subtype.coe_eta` `Quotient.out_eq`
`units_smul_of_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Units` `Module.Ray` `AddCommGroup.toAddCommMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `Units.instGroup` `Units.instDistribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.smulCommClass_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `instNegRay`	—	`Units.smulCommClass_right` `smulCommClass_self` `neg_neg` `neg_units_smul` `units_smul_of_pos` `Units.val_neg` `Right.neg_pos_iff` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`units_smul_of_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Units` `Module.Ray` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `Units.instGroup` `Units.instDistribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.smulCommClass_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid`	—	`ind` `Units.smulCommClass_right` `smulCommClass_self` `smul_ne_zero_iff_ne` `smul_rayOfNeZero` `ray_eq_iff` `SameRay.sameRay_pos_smul_left` `IsOrderedModule.toSMulPosMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left`

RayVector

Definitions

Name	Category	Theorems
`Setoid` 📖	CompOp	3 math math: `equiv_iff_sameRay`, `equiv_neg_iff`, `Module.Ray.someRayVector_ray`
`instInvolutiveNeg` 📖	CompOp	—
`instNeg` 📖	CompOp	2 math math: `coe_neg`, `equiv_neg_iff`
`mapLinearEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_neg` 📖	mathematical	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `RayVector` `instNeg` `NegZeroClass.toNeg`	—	—
`equiv_neg_iff` 📖	mathematical	—	`RayVector` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Setoid` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instNeg`	—	`sameRay_neg_iff`

SameRay

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`SameRay`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`eq_or_ne` `zero_add` `add_zero` `zero_right` `exists_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `add_pos'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_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.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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`
`add_right` 📖	mathematical	`SameRay`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`symm` `add_left`
`exists_eq_smul` 📖	mathematical	`SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `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` `Module.toDistribMulAction`	—	`exists_eq_smul_add`
`exists_eq_smul_add` 📖	mathematical	`SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `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` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsStrictOrderedRing.toZeroLEOneClass` `zero_add` `zero_smul` `one_smul` `add_zero` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LT.lt.le` `add_div` `add_comm` `div_self` `LT.lt.ne'` `div_eq_inv_mul` `SemigroupAction.mul_smul` `smul_add` `add_smul` `inv_smul_smul₀`
`exists_nonneg_left` 📖	mathematical	`SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `Module.toDistribMulAction`	—	`eq_or_ne` `le_rfl` `zero_smul` `le_of_lt` `exists_pos_left`
`exists_nonneg_right` 📖	mathematical	`SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `Module.toDistribMulAction`	—	`exists_nonneg_left` `symm`
`exists_pos` 📖	mathematical	`SameRay`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`exists_pos_left` 📖	mathematical	`SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `Module.toDistribMulAction`	—	`exists_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `SemigroupAction.mul_smul` `inv_smul_smul₀` `LT.lt.ne'`
`exists_pos_right` 📖	mathematical	`SameRay` `Semifield.toCommSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `Module.toDistribMulAction`	—	`exists_pos_left` `symm`
`map` 📖	mathematical	`SameRay`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.map_smul`
`neg` 📖	mathematical	`SameRay` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sameRay_neg_iff`
`nonneg_smul_left` 📖	mathematical	`SameRay` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`symm` `nonneg_smul_right`
`nonneg_smul_right` 📖	mathematical	`SameRay` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`trans` `sameRay_nonneg_smul_right` `smul_zero`
`of_neg` 📖	—	`SameRay` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`sameRay_neg_iff`
`of_subsingleton` 📖	mathematical	—	`SameRay`	—	`zero_left`
`of_subsingleton'` 📖	mathematical	—	`SameRay`	—	`of_subsingleton` `Module.subsingleton`
`pos_smul_left` 📖	mathematical	`SameRay` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`nonneg_smul_left` `LT.lt.le`
`pos_smul_right` 📖	mathematical	`SameRay` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`nonneg_smul_right` `LT.lt.le`
`refl` 📖	mathematical	—	`SameRay`	—	`zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`rfl` 📖	mathematical	—	`SameRay`	—	`refl`
`sameRay_comm` 📖	mathematical	—	`SameRay`	—	`symm`
`sameRay_map_iff` 📖	mathematical	—	`SameRay` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike`	—	`RingHomInvPair.ids` `Function.Injective.sameRay_map_iff` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `EquivLike.injective`
`sameRay_nonneg_smul_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SameRay` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`symm` `sameRay_nonneg_smul_right`
`sameRay_nonneg_smul_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SameRay` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`LE.le.eq_or_lt'` `algebraMap_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `algebraMap_smul` `zero_smul` `zero_right` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `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` `algebraMap.coe_mul` `algebraMap.coe_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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_pf_right`
`sameRay_pos_smul_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SameRay` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`sameRay_nonneg_smul_left` `LT.lt.le`
`sameRay_pos_smul_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`SameRay` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`sameRay_nonneg_smul_right` `LT.lt.le`
`smul` 📖	mathematical	`SameRay`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`map`
`trans` 📖	—	`SameRay` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`eq_or_ne` `zero_left` `zero_right` `exists_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `SemigroupAction.mul_smul` `SMulCommClass.smul_comm` `smulCommClass_self`
`zero_left` 📖	mathematical	—	`SameRay` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`zero_right` 📖	mathematical	—	`SameRay` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`RayVector` 📖	CompOp	5 math math: `equiv_iff_sameRay`, `RayVector.coe_neg`, `instNonemptyRayVectorOfNontrivial`, `RayVector.equiv_neg_iff`, `Module.Ray.someRayVector_ray`
`SameRay` 📖	MathDef	68 math math: `AffineSubspace.sOppSide_iff_exists_right`, `SameRay.of_subsingleton'`, `sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent`, `exists_pos_right_iff_sameRay`, `exists_nonneg_left_iff_sameRay`, `AffineSubspace.sSameSide_iff_exists_left`, `sameRay_iff_inv_norm_smul_eq_of_ne`, `AffineSubspace.sOppSide_iff_exists_left`, `Complex.sameRay_of_arg_eq`, `norm_injOn_ray_right`, `SameRay.sameRay_comm`, `Wbtw.sameRay_vsub_right`, `equiv_iff_sameRay`, `Orientation.oangle_eq_zero_iff_sameRay`, `Orientation.angle_eq_iff_oangle_eq_or_sameRay`, `SameRay.sameRay_nonneg_smul_left`, `sameRay_iff_of_norm_eq`, `SameRay.zero_right`, `AffineSubspace.wOppSide_iff_exists_left`, `sameRay_smul_left_iff`, `SameRay.refl`, `Wbtw.sameRay_vsub_left`, `mem_segment_iff_sameRay`, `sameRay_smul_left_iff_of_ne`, `sameRay_of_mem_orbit`, `sameRay_iff_norm_add`, `exists_nonneg_right_iff_sameRay`, `not_sameRay_iff_of_norm_eq`, `sameRay_neg_smul_left_iff_of_ne`, `isConnected_setOf_sameRay_and_ne_zero`, `AffineSubspace.wSameSide_iff_exists_left`, `exists_pos_left_iff_sameRay`, `Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay`, `SameRay.sameRay_nonneg_smul_right`, `not_sameRay_iff_abs_lt_norm_sub`, `sameRay_neg_swap`, `sameRay_iff_inv_norm_smul_eq`, `SameRay.zero_left`, `not_sameRay_iff_norm_add_lt`, `SameRay.of_subsingleton`, `sameRay_smul_right_iff_of_ne`, `sameRay_neg_smul_right_iff_of_ne`, `sameRay_iff_norm_sub`, `SameRay.sameRay_map_iff`, `sameRay_neg_smul_right_iff`, `AffineSubspace.sSameSide_iff_exists_right`, `sameRay_or_sameRay_neg_iff_not_linearIndependent`, `AffineSubspace.wSameSide_iff_exists_right`, `Complex.sameRay_iff`, `Complex.sameRay_iff_arg_div_eq_zero`, `SameRay.rfl`, `SameRay.sameRay_pos_smul_right`, `ray_eq_iff`, `Orientation.oangle_eq_pi_iff_sameRay_neg`, `sameRay_smul_right_iff`, `exists_pos_left_iff_sameRay_and_ne_zero`, `sameRay_neg_smul_left_iff`, `sameRay_of_mem_segment`, `AffineSubspace.wOppSide_iff_exists_right`, `Wbtw.sameRay_vsub`, `SameRay.sameRay_pos_smul_left`, `norm_injOn_ray_left`, `isConnected_setOf_sameRay`, `Function.Injective.sameRay_map_iff`, `sameRay_iff_norm_smul_eq`, `wbtw_iff_sameRay_vsub`, `sameRay_neg_iff`, `exists_pos_right_iff_sameRay_and_ne_zero`
`instMulActionRay` 📖	CompOp	11 math math: `units_inv_smul`, `Module.Ray.neg_units_smul`, `Module.Ray.units_smul_of_neg`, `smul_rayOfNeZero`, `Module.Ray.linearEquiv_smul_eq_map`, `units_smul_eq_self_iff`, `units_smul_eq_neg_iff`, `Module.Ray.units_smul_of_pos`, `Orientation.map_eq_det_inv_smul`, `Module.Basis.map_orientation_eq_det_inv_smul`, `Module.Basis.orientation_unitsSMul`
`instMulActionRayVector` 📖	CompOp	—
`instNegRay` 📖	CompOp	23 math math: `Orientation.ne_iff_eq_neg`, `Module.Ray.neg_units_smul`, `Orientation.volumeForm_neg_orientation`, `Orientation.eq_or_eq_neg`, `Module.Ray.units_smul_of_neg`, `Orientation.map_eq_neg_iff_det_neg`, `Orientation.areaForm_neg_orientation`, `Orientation.reindex_neg`, `units_smul_eq_neg_iff`, `Module.Basis.orientation_eq_or_eq_neg`, `Orientation.kahler_neg_orientation`, `neg_rayOfNeZero`, `Module.Basis.orientation_ne_iff_eq_neg`, `Orientation.rotation_neg_orientation_eq_neg`, `Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg`, `Orientation.map_neg`, `Orientation.rightAngleRotation_trans_neg_orientation`, `Orientation.volumeForm_zero_neg`, `Module.Ray.map_neg`, `Module.Basis.orientation_neg_single`, `Orientation.eq_or_eq_neg_of_isEmpty`, `Orientation.oangle_neg_orientation_eq_neg`, `Orientation.rightAngleRotation_neg_orientation`
`rayOfNeZero` 📖	CompOp	8 math math: `smul_rayOfNeZero`, `neg_rayOfNeZero`, `Module.Ray.someVector_ray`, `ray_pos_smul`, `Module.Ray.map_apply`, `Orientation.reindex_apply`, `Orientation.map_apply`, `ray_eq_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_sameRay_neg_smul_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SameRay` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsDomain.toIsCancelMulZero` `LT.lt.ne` `smul_eq_zero` `sub_smul` `smul_smul` `sub_eq_zero` `ne_of_gt` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `LT.lt.trans` `mul_neg_of_pos_of_neg` `IsStrictOrderedRing.toPosMulStrictMono`
`eq_zero_of_sameRay_self_neg` 📖	mathematical	`SameRay` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`NegZeroClass.toZero`	—	`eq_zero_of_sameRay_neg_smul_right` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_lt_one'` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `neg_one_smul`
`equiv_iff_sameRay` 📖	mathematical	—	`RayVector` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `RayVector.Setoid` `SameRay`	—	—
`exists_nonneg_left_iff_sameRay` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `SameRay` `Semifield.toCommSemiring`	—	`SameRay.sameRay_nonneg_smul_right` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left` `SameRay.exists_nonneg_left`
`exists_nonneg_right_iff_sameRay` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `SameRay` `Semifield.toCommSemiring`	—	`SameRay.sameRay_comm` `exists_nonneg_left_iff_sameRay`
`exists_pos_left_iff_sameRay` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `SameRay` `Semifield.toCommSemiring`	—	`SameRay.sameRay_pos_smul_right` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left` `SameRay.exists_pos_left`
`exists_pos_left_iff_sameRay_and_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `SameRay` `Semifield.toCommSemiring`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `LT.lt.le` `LT.lt.ne'` `exists_pos_left_iff_sameRay`
`exists_pos_right_iff_sameRay` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `SameRay` `Semifield.toCommSemiring`	—	`SameRay.sameRay_comm` `exists_pos_left_iff_sameRay`
`exists_pos_right_iff_sameRay_and_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `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` `SameRay` `Semifield.toCommSemiring`	—	`SameRay.sameRay_comm` `exists_pos_left_iff_sameRay_and_ne_zero`
`instNonemptyRayOfNontrivial` 📖	mathematical	—	`Module.Ray`	—	`Nonempty.map` `instNonemptyRayVectorOfNontrivial`
`instNonemptyRayVectorOfNontrivial` 📖	mathematical	—	`RayVector`	—	`exists_ne`
`neg_rayOfNeZero` 📖	mathematical	—	`Module.Ray` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instNegRay` `rayOfNeZero` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NegZeroClass.toZero` `neg_ne_zero`	—	—
`ray_eq_iff` 📖	mathematical	—	`rayOfNeZero` `SameRay`	—	`Quotient.eq'`
`ray_pos_smul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`rayOfNeZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`ray_eq_iff` `SameRay.sameRay_pos_smul_left` `IsOrderedModule.toSMulPosMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left`
`sameRay_neg_iff` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smul_neg`
`sameRay_neg_smul_left_iff` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toZero`	—	`SameRay.sameRay_comm` `sameRay_neg_smul_right_iff`
`sameRay_neg_smul_left_iff_of_ne` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`SameRay.sameRay_comm` `sameRay_neg_smul_right_iff_of_ne`
`sameRay_neg_smul_right_iff` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toZero`	—	`sameRay_neg_iff` `neg_neg` `neg_smul` `sameRay_smul_right_iff` `neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`sameRay_neg_smul_right_iff_of_ne` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Ne.le_iff_lt`
`sameRay_neg_swap` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sameRay_neg_iff` `neg_neg`
`sameRay_of_mem_orbit` 📖	mathematical	`Set` `Set.instMembership` `MulAction.orbit` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Units.posSubgroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Subgroup.instDistribMulActionSubtypeMem` `Units.instDistribMulAction` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`SameRay` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`SameRay.sameRay_pos_smul_left` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left`
`sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `CommSemiring.toSemiring`	—	`sameRay_or_sameRay_neg_iff_not_linearIndependent` `SameRay.congr_simp` `neg_zero`
`sameRay_or_sameRay_neg_iff_not_linearIndependent` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `CommSemiring.toSemiring`	—	`SameRay.congr_simp` `LinearIndependent.ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `neg_zero` `Fin.sum_univ_two` `Matrix.cons_val_fin_one` `neg_smul` `add_neg_cancel` `LT.lt.ne` `neg_eq_zero` `smul_neg` `neg_add_cancel` `lt_trichotomy` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `add_eq_zero_iff_eq_neg` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_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.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.neg_eq_eval` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `eq_intCast` `Int.cast_neg` `Int.cast_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `zero_smul` `IsDomain.toIsCancelMulZero` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE` `not_and_or`
`sameRay_smul_left_iff` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`SameRay.sameRay_comm` `sameRay_smul_right_iff`
`sameRay_smul_left_iff_of_ne` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`SameRay.sameRay_comm` `sameRay_smul_right_iff_of_ne`
`sameRay_smul_right_iff` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`eq_zero_of_sameRay_neg_smul_right` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE` `not_le` `SameRay.sameRay_nonneg_smul_right` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left` `SameRay.zero_left`
`sameRay_smul_right_iff_of_ne` 📖	mathematical	—	`SameRay` `CommRing.toCommSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Ne.le_iff_lt`
`smul_rayOfNeZero` 📖	mathematical	—	`Module.Ray` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `rayOfNeZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smul_ne_zero_iff_ne`	—	—
`units_inv_smul` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.Ray` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `Units.instGroup` `Units.instDistribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.smulCommClass_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Units.instInv`	—	`mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_lt_of_covariant_le` `Units.ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Units.smulCommClass_right` `smulCommClass_self` `Module.Ray.units_smul_of_pos` `SemigroupAction.mul_smul` `smul_inv_smul`
`units_smul_eq_neg_iff` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.Ray` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `Units.instGroup` `Units.instDistribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.smulCommClass_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `instNegRay` `Preorder.toLT` `PartialOrder.toPreorder` `Units.val` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Units.smulCommClass_right` `smulCommClass_self` `neg_neg` `Module.Ray.neg_units_smul` `units_smul_eq_self_iff` `Units.val_neg` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`units_smul_eq_self_iff` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.Ray` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `instMulActionRay` `Units.instGroup` `Units.instDistribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Units.smulCommClass_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Units.val`	—	`Module.Ray.ind` `Units.smulCommClass_right` `smulCommClass_self` `smul_ne_zero_iff_ne` `sameRay_smul_left_iff_of_ne` `Units.ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero`

---

← Back to Index