SameRay.add_left
theorem SameRay.add_left :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y z : M}, SameRay R x z → SameRay R y z → SameRay R (x + y) z
The theorem `SameRay.add_left` states that for any type `R` with a strict ordered commutative semiring structure, type `M` with an additive commutative monoid structure and a module structure over `R`, and for any three elements `x`, `y`, and `z` of `M`, if `x` and `y` are in the same ray as `z` (meaning that they are either zero or some positive multiples of them are equal), then their sum `x + y` is also in the same ray as `z`.
More concisely: If `x`, `y` are in the same ray as `z` in an additive commutative monoid `M` over a strict ordered commutative semiring `R`, then `x + y` is also in the same ray as `z`.
|
eq_zero_of_sameRay_self_neg
theorem eq_zero_of_sameRay_self_neg :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x : M} [inst_3 : NoZeroSMulDivisors R M], SameRay R x (-x) → x = 0
The theorem `eq_zero_of_sameRay_self_neg` states that for any type `R` that is a strict ordered commutative ring and any type `M` that is an additive commutative group and is a module over `R`, if a vector `x` from `M` is in the same ray as its negation (as per the `SameRay` definition), then the vector `x` must be zero. This statement holds true given there are no nonzero scalar multipliers that result in a zero vector in `M` (indicated by `NoZeroSMulDivisors R M`). In simpler terms, if a vector and its negation are at the same direction, the vector is necessarily a zero vector.
More concisely: If `R` is a strict ordered commutative ring, `M` is an additive commutative group and a module over `R` with no nonzero scalar multipliers resulting in a zero vector, and `x` is an element of `M` such that `x = -x`, then `x` is equal to the zero vector.
|
equiv_iff_sameRay
theorem equiv_iff_sameRay :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {v₁ v₂ : RayVector R M}, v₁ ≈ v₂ ↔ SameRay R ↑v₁ ↑v₂
This theorem establishes an equivalence between two nonzero vectors in terms of their "sameness" in a ray. For any strict ordered commutative semiring `R`, additive commutative monoid `M` and module `M` over `R`, two nonzero vectors `v₁` and `v₂` are equivalent if and only if they lie in the same ray in `R`. In other words, the two nonzero vectors `v₁` and `v₂` are equivalent if either one of them is the zero vector, or there exist positive scalars `r₁` and `r₂` such that `r₁` times `v₁` equals `r₂` times `v₂`.
More concisely: For any strict ordered commutative semiring `R`, additive commutative monoid `M`, and module `M` over `R`, two nonzero vectors `v₁` and `v₂` in `M` are equivalent if and only if there exist positive scalars `r₁` and `r₂` such that `r₁ * v₁ = r₂ * v₂`.
|
SameRay.sameRay_map_iff
theorem SameRay.sameRay_map_iff :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {x y : M} (e : M ≃ₗ[R] N),
SameRay R (e x) (e y) ↔ SameRay R x y
The theorem "SameRay.sameRay_map_iff" states that for any given vectors 'x' and 'y' in a module 'M' over a strictly ordered commutative semiring 'R', and a linear equivalence 'e' between module 'M' and another module 'N', the images of these vectors under the linear equivalence 'e' are in the same ray if and only if the original vectors 'x' and 'y' are in the same ray. Here, vectors being in the same ray is defined as either one of the vectors is zero, or there exist positive multiples of the vectors that are equal.
More concisely: For vectors x and y in module M over a strictly ordered commutative semiring R, and a linear equivalence e between M and N, x and y are in the same ray if and only if e(x) and e(y) are.
|
SameRay.rfl
theorem SameRay.rfl :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x : M}, SameRay R x x
The theorem `SameRay.rfl` states that for any type `R` that is a strict ordered commutative semiring, and any type `M` that is an additive commutative monoid and also a module over `R`, any vector `x` from `M` is in the same ray as itself. This essentially states the reflexivity property of the `SameRay` relation in the context of vectors in a module over a semiring, i.e., every vector is in the same direction as itself.
More concisely: For any strict ordered commutative semiring `R` and any additive commutative monoid `M` that is an `R`-module, every vector `x` in `M` is in the same ray as `x` regarding the `SameRay` relation.
|
ray_eq_iff
theorem ray_eq_iff :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {v₁ v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0),
rayOfNeZero R v₁ hv₁ = rayOfNeZero R v₂ hv₂ ↔ SameRay R v₁ v₂
The theorem `ray_eq_iff` states that for any type `R` with a strict ordered commutative semiring structure, any type `M` with an additive commutative monoid structure and a module over `R`, and any two nonzero vectors `v₁` and `v₂` from `M`, the rays given by `v₁` and `v₂` are equal if and only if `v₁` and `v₂` satisfy the `SameRay` condition. In the context of this theorem, `SameRay` condition is satisfied if either one of `v₁` or `v₂` is zero, or there exist some positive multiples `r₁` and `r₂` of `v₁` and `v₂` respectively, such that `r₁ • v₁ = r₂ • v₂` (where `•` denotes scalar multiplication).
More concisely: For any strict ordered commutative semiring `R`, additive commutative monoid `M` over `R` with module structure, and nonzero vectors `v₁` and `v₂` in `M`, `Ray v₁ = Ray v₂` if and only if there exist positive multiples `r₁` and `r₂` such that `r₁ • v₁ = r₂ • v₂`.
|
SameRay.exists_pos
theorem SameRay.exists_pos :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M}, SameRay R x y → x ≠ 0 → y ≠ 0 → ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
The theorem `SameRay.exists_pos` states that for any strict ordered commutative semiring `R` and any additive commutative monoid `M` which is also an `R`-module, if `x` and `y` are nonzero vectors in `M` that lie on the same ray (as defined by the `SameRay` relation), then there exist positive elements `r₁` and `r₂` in `R` such that `r₁` times `x` equals `r₂` times `y`. In other words, if two nonzero vectors point in the same direction, we can find positive scalars making them equal.
More concisely: For any strict ordered commutative semiring `R`, additive commutative monoid `M` being an `R`-module, and nonzero vectors `x` and `y` in `M` on the same ray, there exist positive elements `r₁, r₂` in `R` such that `r₁ * x = r₂ * y`.
|
Module.Ray.linearEquiv_smul_eq_map
theorem Module.Ray.linearEquiv_smul_eq_map :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (e : M ≃ₗ[R] M) (v : Module.Ray R M), e • v = (Module.Ray.map e) v
This theorem asserts that, for any strict ordered commutative semiring `R`, and any module `M` over `R`, the action of a linear equivalence `e` on a 'ray' in the module `M` via scalar multiplication (`e • v`) is equivalent to mapping the 'ray' with the same linear equivalence (`Module.Ray.map e v`). Here, 'rays' in the module are represented as equivalence classes of nonzero vectors that share common positive multiples. The theorem is essentially stating that these two operations on 'rays' in the module - scalar multiplication and mapping through a linear equivalence - yield the same result.
More concisely: For any strict ordered commutative semiring `R`, and module `M` over `R`, the scalar multiplication action of a linear equivalence `e` on the ray of a nonzero vector `v` in `M` is equal to mapping the ray of `v` with `e`.
|
SameRay.neg
theorem SameRay.neg :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x y : M}, SameRay R x y → SameRay R (-x) (-y)
The theorem `SameRay.neg` states that for any strict ordered commutative ring `R`, any additive commutative group `M`, any `R`-module `M`, and any vectors `x` and `y` in `M`, if `x` and `y` are in the same ray (meaning either one of them is the zero vector or a positive scalar multiple of one is equal to the other), then the negatives of `x` and `y` (i.e., `-x` and `-y`) are also in the same ray. This theorem is the if-and-only-if version of `SameRay.neg`.
More concisely: If vectors `x` and `y` in an additive commutative group `M` of an ordered commutative ring `R`, where `M` is an `R`-module, lie on the same ray (i.e., one is a positive scalar multiple of the other or both are zero), then their negatives `-x` and `-y` also lie on the same ray.
|
SameRay.sameRay_pos_smul_left
theorem SameRay.sameRay_pos_smul_left :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M]
[inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S} (v : M), 0 < a → SameRay R (a • v) v
This theorem states that, for any strictly ordered commutative semiring `R`, additively commutative monoid `M`, ordered commutative semiring `S`, given an algebra from `S` to `R` and a module structure of `M` over `S` and `R`, with positivity-preserving scalar multiplication and scalar tower properties, if `a` is a positive element of `S` and `v` is a vector in `M`, then `a • v` (which means `a` times `v`) and `v` are in the same ray. In simpler terms, multiplying a vector by a positive scalar does not change the 'direction' of the vector, as per the definition of "SameRay".
More concisely: For any commutative semirings `R` and `S`, additively commutative monoid `M`, and positive element `a` in `S`, if `a` acts multiplicatively as an algebra homomorphism from `S` to `R`, `M` is an `S`-module and `R`-module with positivity-preserving scalar multiplication and scalar tower properties, then for all `v` in `M`, `a • v` and `v` are in the same ray.
|
Module.Ray.ind
theorem Module.Ray.ind :
∀ (R : Type u_1) [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {C : Module.Ray R M → Prop},
(∀ (v : M) (hv : v ≠ 0), C (rayOfNeZero R v hv)) → ∀ (x : Module.Ray R M), C x
This theorem, `Module.Ray.ind`, provides an induction principle for the type `Module.Ray` in the context of a module over a strictly ordered commutative semiring. Given any type `R` with a strictly ordered commutative semiring structure, type `M` with an additive commutative monoid structure, and a module structure over `R` and `M`, it says that for any property `C` that might hold for an element of `Module.Ray R M`, if we can prove that this property `C` holds for every nonzero vector `v` in `M` (which is encapsulated by the `rayOfNeZero` function), then we can conclude that this property `C` holds for every element in `Module.Ray R M`.
More concisely: If a property holds for every nonzero vector in a module over a strictly ordered commutative semiring, then it holds for every element in the corresponding Module.Ray.
|
SameRay.smul
theorem SameRay.smul :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M} {S : Type u_6} [inst_3 : Monoid S] [inst_4 : DistribMulAction S M]
[inst_5 : SMulCommClass R S M], SameRay R x y → ∀ (s : S), SameRay R (s • x) (s • y)
The theorem `SameRay.smul` states that, given a strict ordered commutative semiring `R` and an additive commutative monoid `M` that is also a module over `R`, if two vectors `x` and `y` from `M` are on the same ray (meaning either one of them is zero or there exist positive multiples `r₁` and `r₂` such that `r₁ • x = r₂ • y`), then for any scalar `s` from a monoid `S` that distributes over the multiplication action on `M` and commutes with the scalar multiplication of `R` on `M`, the vectors `s • x` and `s • y` are also on the same ray. In other words, scaling the vectors `x` and `y` by the same factor preserves the property that they are on the same ray.
More concisely: If vectors `x` and `y` in an additive commutative monoid `M` over a strict ordered commutative semiring `R` with distributive monoid scalar multiplication `S` are on the same ray, then scaling them by the same scalar in `S` preserves their equivalence on the ray.
|
Module.Ray.units_smul_of_pos
theorem Module.Ray.units_smul_of_pos :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (u : Rˣ), 0 < ↑u → ∀ (v : Module.Ray R M), u • v = v
This theorem states that, for any strictly ordered commutative semiring `R`, an addable commutative monoid `M`, and `M` being a module over `R`, scaling a "ray" (equivalence class of non-zero vectors that have common positive multiples) in the module `M` by a positive unit `u` from `R` doesn't change the ray. In other words, for any positive unit `u` in `R` and any ray `v` in `M`, the result of scaling `v` by `u` is still `v`. This can be interpreted as the fact that scaling doesn't change the direction of a ray, which is only determined by the equivalence class of vectors it represents, not by their magnitudes.
More concisely: For any strictly ordered commutative semiring `R`, any additive commutative monoid `M` that is an `R`-module, and any positive unit `u` in `R` and ray `v` in `M`, scaling `v` by `u` results in the same ray.
|
SameRay.sameRay_nonneg_smul_right
theorem SameRay.sameRay_nonneg_smul_right :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M]
[inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S} (v : M), 0 ≤ a → SameRay R v (a • v)
The theorem `SameRay.sameRay_nonneg_smul_right` asserts that for any vector `v`, a nonnegative scalar multiple of `v` is in the 'same ray' as `v` itself. Here, 'same ray' means that two vectors are considered the same if either one of them is zero, or if there exist positive multiples of them that are equal. This property holds in any context where the scalars form a strict ordered commutative semiring and act on a commutative additive monoid to form a module, with the additional structure that the scalar multiplication is positive monotonic and there exists a scalar tower.
More concisely: For any vector `v` and nonnegative scalar `r`, `r * v` lies on the same ray as `v` in the context of a commutative additive monoid with a positive monotonic scalar multiplication over a strict ordered commutative semiring, where there exists a scalar tower.
|
SameRay.exists_nonneg_left
theorem SameRay.exists_nonneg_left :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x y : M}, SameRay R x y → x ≠ 0 → ∃ r, 0 ≤ r ∧ r • x = y
The theorem states that for any linear ordered field `R` and an additive commutative group `M` that is also a module over `R`, if we have two vectors `x` and `y` such that `x` is not zero and `y` is on the same ray as `x` (meaning either `y` is zero or there exist positive scalars `r₁` and `r₂` such that `r₁ * x = r₂ * y`), then there exists a non-negative scalar `r` such that `r * x = y`. Thus, if `y` is in the same direction as `x`, it is a scaled version of `x` by a non-negative scalar.
More concisely: Given a linear ordered field `R` and an additive commutative `R`-module `M`, if non-zero vector `x` in `M` and vector `y` are on the same ray, then there exists a non-negative scalar `r` such that `y = r * x`.
|
neg_rayOfNeZero
theorem neg_rayOfNeZero :
∀ (R : Type u_1) [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(v : M) (h : v ≠ 0), -rayOfNeZero R v h = rayOfNeZero R (-v) ⋯
The theorem `neg_rayOfNeZero` states that for any strict ordered commutative ring `R` and any additive commutative group `M` which is also a module over `R`, if `v` is a non-zero element of `M`, then the ray given by the negation of `v` is equal to the ray of the negation of `v`. In other words, negating the ray given by a non-zero vector `v` in the module equals the ray given by the negation of `v` itself.
More concisely: For any strict ordered commutative ring `R`, additive commutative group `M` being an `R`-module, and non-zero `v` in `M`, the negation of the ray generated by `v` is equal to the ray generated by the negation of `v`.
|
sameRay_or_sameRay_neg_iff_not_linearIndependent
theorem sameRay_or_sameRay_neg_iff_not_linearIndependent :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {x y : M}, SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
The theorem `sameRay_or_sameRay_neg_iff_not_linearIndependent` states that, given two vectors 'x' and 'y' in a module 'M' over a linearly ordered commutative ring 'R', the vectors 'x' and 'y' are either in the same ray or 'x' is in the same ray as the negation of 'y', if and only if the set containing 'x' and 'y' is not linearly independent. This means that 'x' and 'y' are linearly dependent, i.e., there exists a non-trivial linear combination of them that equals zero, if and only if they share a common ray, or 'x' shares a common ray with the negation of 'y'. The condition of same ray between two vectors is defined as either one of them being zero or the existence of positive multiples of them that are equal.
More concisely: Two vectors x and y in a linearly ordered commutative ring R's module M are in the same ray or x is in the same ray as the negation of y if and only if they are linearly dependent.
|
Function.Injective.sameRay_map_iff
theorem Function.Injective.sameRay_map_iff :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {x y : M} {F : Type u_6}
[inst_5 : FunLike F M N] [inst_6 : LinearMapClass F R M N] {f : F},
Function.Injective ⇑f → (SameRay R (f x) (f y) ↔ SameRay R x y)
This theorem states that for any strict ordered commutative semiring `R`, types `M` and `N` with additively commutative monoid and `R`-module structures, vectors `x` and `y` of type `M`, a function-like type `F` from `M` to `N`, and an injective `R`-linear map `f` of type `F`, the images of the vectors `x` and `y` under the map `f` are on the same ray if and only if the original vectors `x` and `y` are on the same ray. In mathematical terms, if two vectors are scalar multiples of each other (or one of them is the zero vector), then their images under an injective linear map are also scalar multiples of each other (or one of them is the zero vector), and vice versa.
More concisely: For any strict ordered commutative semiring `R`, injective `R`-linear map `f`, and vectors `x` and `y` in additively commutative `R`-modules `M` and `N`, if `x` and `y` are on the same ray (i.e., scalar multiples), then their images `f(x)` and `f(y)` are also on the same ray; conversely, if `f(x)` and `f(y)` are on the same ray, then `x` and `y` are scalar multiples.
|
RayVector.coe_neg
theorem RayVector.coe_neg : ∀ {M : Type u_2} [inst : AddCommGroup M] {R : Type u_4} (v : RayVector R M), ↑(-v) = -↑v
The theorem `RayVector.coe_neg` states that for any type `M` that forms an additive commutative group and any nonzero vector `v` of type `RayVector R M`, the negation of `v` when coerced to the underlying module `M` is equal to the negation of `v` after it has been coerced to `M`. In other words, negating a nonzero vector before or after coercing it to the underlying module yields the same result.
More concisely: For any additive commutative group type `M` and nonzero vector `v` of type `RayVector R M`, the negation of `v` when coerced to `M` equals the negation of `v` in `RayVector R M`.
|
SameRay.pos_smul_left
theorem SameRay.pos_smul_left :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M} {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R]
[inst_5 : Module S M] [inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S},
SameRay R x y → 0 < a → SameRay R (a • x) y
The theorem `SameRay.pos_smul_left` states that for any given types `R` and `M`, where `R` is a strictly ordered commutative semiring and `M` is an additive commutative monoid and a module over `R`, and given `x` and `y` in `M`, and `S` is an ordered commutative semiring and an algebra over `R`, and `M` is a module over `S`, and given `a` in `S`, if `x` and `y` are in the same ray (`SameRay R x y`) and `a` is positive (`0 < a`), then the positive multiple of `x` by `a` and `y` are in the same ray (`SameRay R (a • x) y`). In simpler terms, it implies that if a vector `x` and a vector `y` are in the same direction, then any positive scaling of `x` remains in the same direction as `y`.
More concisely: Given types `R` (a strictly ordered commutative semiring), `M` (an additive commutative monoid and an `R`-module), `S` (an ordered commutative semiring and an algebra over `R`), and `M` (an `S`-module), if `x`, `y` ∈ `M` lie on the same ray with respect to `R`, and `a` > 0 ∈ `S`, then `a • x` and `y` lie on the same ray with respect to `R`.
|
SameRay.symm
theorem SameRay.symm :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M}, SameRay R x y → SameRay R y x
The theorem `SameRay.symm` states that for any strict ordered commutative semiring `R` and any additive commutative monoid `M` that is also a module over `R`, the relation `SameRay` is symmetric. In other words, if the vectors `x` and `y` from `M` are in the same ray (i.e., if either of them is zero or some positive multiples of them are equal), then `y` and `x` are also in the same ray.
More concisely: If `x` and `y` are in the same ray in an additive commutative monoid `M` over a strict ordered commutative semiring `R`, then `y` and `x` are also in the same ray.
|
ray_pos_smul
theorem ray_pos_smul :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {v : M} (h : v ≠ 0) {r : R},
0 < r → ∀ (hrv : r • v ≠ 0), rayOfNeZero R (r • v) hrv = rayOfNeZero R v h
This theorem states that for any strict ordered commutative semiring `R`, any additive commutative monoid `M` and any module `M` over `R`, if we have a nonzero vector `v` in `M` and a positive scalar `r` in `R`, the ray given by the positive scalar multiple `r • v` is the same as the ray given by the original nonzero vector `v`. This holds true even if `r • v` is not equal to zero. Here, the ray is defined to be the equivalence class of nonzero vectors under scalar multiplication.
More concisely: For any strict ordered commutative semiring `R`, additive commutative monoid `M`, and `R`-module `M`, if `v` is a nonzero vector in `M` and `r` is a positive scalar in `R`, then the rays generated by `v` and `r • v` are equal.
|
SameRay.zero_left
theorem SameRay.zero_left :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (y : M), SameRay R 0 y
This theorem states that for any type `R` that is a strict ordered commutative semiring, and any type `M` that is an additive commutative monoid and also a module over `R`, any vector `y` from `M` is in the same ray as the zero vector. The concept of "same ray" here is defined as either one of the vectors being zero, or there exists two positive scalar multiples (from the semiring `R`) such that one vector is the scalar multiple of the other.
More concisely: For any strict ordered commutative semiring `R`, any additive commutative monoid `M` that is an `R`-module, and any vectors `x, y` in `M`, either `x = 0` or `y = rx` for some positive scalar `r` in `R`.
|
SameRay.trans
theorem SameRay.trans :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y z : M}, SameRay R x y → SameRay R y z → (y = 0 → x = 0 ∨ z = 0) → SameRay R x z
The theorem `SameRay.trans` states that the property of "being in the same ray" is transitive in a given context of a strict ordered commutative semiring and a module structure over an additive commutative monoid. Specifically, if we have three vectors `x`, `y`, and `z` such that `x` and `y` are in the same ray, and `y` and `z` are also in the same ray, then `x` and `z` are in the same ray provided that if `y` is the zero vector, then either `x` or `z` must also be zero.
In simple terms, this means if we can get from vector `x` to `y`, and from `y` to `z` by multiplying with positive scalars (or if one of them is a zero vector), we can get from `x` to `z` directly, unless `y` is zero and both `x` and `z` are nonzero.
More concisely: If `x`, `y`, and `z` are vectors in a strict ordered commutative semiring with a module structure over an additive commutative monoid, and `x` is in the same ray as both `y` and `z` (with `y` possibly being the zero vector), then `x` and `z` are in the same ray. However, if `y` is the zero vector and neither `x` nor `z` is zero, then this condition does not hold.
|
SameRay.sameRay_comm
theorem SameRay.sameRay_comm :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M}, SameRay R x y ↔ SameRay R y x
This theorem states that for any type `R` with a strict ordered commutative semiring structure, type `M` with both an addition commutative monoid and `R`-module structure, and any two elements `x` and `y` of `M`, the relation `SameRay` between `x` and `y` is symmetric. That is, `x` and `y` are in the same ray if and only if `y` and `x` are in the same ray. In other words, the order of `x` and `y` does not matter in the `SameRay` relation: if `x` and `y` could be related by either of them being zero or some positive multiples of them being equal, then the same applies for `y` and `x`.
More concisely: For any strict ordered commutative semiring `R`, commutative monoid additive `M` over `R`, and all `x, y` in `M`, the relation `SameRay` between `x` and `y` is a symmetric equivalence relation.
|
Mathlib.LinearAlgebra.Ray._auxLemma.2
theorem Mathlib.LinearAlgebra.Ray._auxLemma.2 :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (x : M), SameRay R x 0 = True
This theorem, named `Mathlib.LinearAlgebra.Ray._auxLemma.2`, states that for any type `R` which is a strict ordered commutative semiring, any type `M` which is an additive commutative monoid and a module over `R`, and any element `x` of `M`, `x` and `0` are always in the same ray. In mathematical terms, this means that either `x` is zero or there exists some positive multiples `r₁` and `r₂` of `x` and `0` respectively such that `r₁ * x = r₂ * 0`. However, as `r₂ * 0` is always zero, it means `r₁ * x` must be zero, therefore `x` itself must be zero. Therefore, the theorem essentially states that a vector is in the same ray as the zero vector if and only if it is the zero vector itself.
More concisely: For any strict ordered commutative semiring R, additive commutative monoid and R-module M, and any x in M, x and 0 are in the same ray if and only if x is the zero element of M.
|
units_inv_smul
theorem units_inv_smul :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(u : Rˣ) (v : Module.Ray R M), u⁻¹ • v = u • v
This theorem states that for any linearly ordered commutative ring `R` and any module `M` over `R`, scaling a ray in `M` by the inverse of a unit in `R` is equivalent to scaling the ray by the unit itself. Here, a ray in `M` is an equivalence class of nonzero vectors in `M` that are equivalent if they differ by a positive scalar multiple from `R`. In other words, for any unit `u` in `R` and any ray `v` in `M`, `u⁻¹ • v` equals `u • v`. This theorem is a property of scalar multiplication in modules over a ring.
More concisely: For any unit u in a commutative ring R and any ray v in an R-module M, scaling v by the unit u inverse is equivalent to scaling it by u, i.e., u⁻¹ • v = u • v.
|
SameRay.exists_pos_left
theorem SameRay.exists_pos_left :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x y : M}, SameRay R x y → x ≠ 0 → y ≠ 0 → ∃ r, 0 < r ∧ r • x = y
The theorem `SameRay.exists_pos_left` states that for all types `R` being a linear ordered field, and for all types `M` being an additive commutative group and a module over `R`, if two vectors `x` and `y` are in the same ray (meaning either one of them is zero, or some positive multiples of them are equal) and both `x` and `y` are non-zero, then there exists a positive real number `r` such that `r` times `x` equals `y`. In other words, if two non-zero vectors are in the same ray, one is a positive scalar multiple of the other.
More concisely: Given a linear ordered field R and an additive commutative group M being an R-module, if non-zero vectors x and y in M lie on the same ray, then there exists a positive r in R such that rx = y.
|
SameRay.exists_eq_smul_add
theorem SameRay.exists_eq_smul_add :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{v₁ v₂ : M}, SameRay R v₁ v₂ → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
The theorem states that if two vectors, `v₁` and `v₂`, belong to the same ray in a linearly ordered field `R` with an associated module `M`, then there exist nonnegative scalars `a` and `b` such that `a + b` equals 1, and `v₁` and `v₂` can be expressed as `a • (v₁ + v₂)` and `b • (v₁ + v₂)`, respectively. In other words, `v₁` and `v₂` can be expressed as a linear combination of themselves, with the coefficients summing to 1.
More concisely: If two vectors `v₁` and `v₂` in a linearly ordered field `R` with module `M` lie on the same ray, then there exist nonnegative scalars `a` and `b` such that `a + b = 1` and `v₁ = a * (v₁ + v₂)` and `v₂ = b * (v₁ + v₂)`.
|
SameRay.sameRay_pos_smul_right
theorem SameRay.sameRay_pos_smul_right :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M]
[inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S} (v : M), 0 < a → SameRay R v (a • v)
The theorem states that for any vector `v` and any positive scalar `a` in an ordered commutative semiring `S`, the vector `v` is in the "same ray" as `a` times `v`. Here "same ray" is defined for types `R` and `M` where `R` is a strictly ordered commutative semiring and `M` is a module over `R`. Two vectors are in the same ray if one of them is zero, or there exist positive multiples of each that are equal. The theorem assumes the necessary algebraic structures to talk about scalar multiplication and order, and that scalar multiplication by positive elements of `S` is monotone in the `R` component. Also, it assumes that `S` is a subring of `R` and `S` scalars can be multiplied with `M` vectors.
More concisely: For any vector `v` in a module `M` over a strictly ordered commutative semiring `S`, and any positive scalar `a` in `S`, the vectors `v` and `a`∘`v` (scalar multiplication) are in the same ray.
|
SameRay.nonneg_smul_left
theorem SameRay.nonneg_smul_left :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M} {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R]
[inst_5 : Module S M] [inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S},
SameRay R x y → 0 ≤ a → SameRay R (a • x) y
The theorem `SameRay.nonneg_smul_left` states that if two vectors, let's call them x and y, are in the same ray (which in the context of vector spaces means that either one of them is zero or some positive multiples of them are equal), then a nonnegative scalar multiple of x is also in the same ray as y. It's important to note that this theorem is applicable in the context of a strict ordered commutative semiring R and a module M, where the scalar field of the vectors is R. The scalar multiple of x is taken from another ordered commutative semiring S which is associated with R through an algebra structure.
More concisely: If vectors x and y are in the same ray in a module M over a strict ordered commutative semiring R, then a nonnegative scalar multiple of x is also in the same ray as y.
|
Module.Ray.someVector_ray
theorem Module.Ray.someVector_ray :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (x : Module.Ray R M), rayOfNeZero R x.someVector ⋯ = x
This theorem, `Module.Ray.someVector_ray`, asserts that for any strict ordered commutative semiring `R`, any addtive commutative monoid `M` that is a module over `R`, and any ray `x` in the module, the ray of `x.someVector` (constructed using the `rayOfNeZero` function) is equal to the original ray `x`. In other words, the ray of the non-zero vector representing a given ray in the module is the same as the original ray, ensuring consistency in the representation of rays in the module.
More concisely: For any strict ordered commutative semiring R, additive commutative monoid M as an R-module, and ray x in M, the ray of x's non-zero vector (constructed using `rayOfNeZero`) is equal to ray x.
|
SameRay.pos_smul_right
theorem SameRay.pos_smul_right :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M} {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R]
[inst_5 : Module S M] [inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S},
SameRay R x y → 0 < a → SameRay R x (a • y)
This theorem states that, given a strict ordered commutative semiring `R`, an additive commutative monoid `M` that is also a module over `R`, a vector `x` and a vector `y` in `M`, a strictly positive scalar `a` which belongs to another ordered commutative semiring `S` that is also an algebra over `R`, if `x` and `y` lie on the same ray (which means that either `x` or `y` is zero, or there exist two positive scalars such that the scalar multiple of `x` by the first scalar is equal to the scalar multiple of `y` by the second scalar), then `x` and the scalar multiple of `y` by `a` also lie on the same ray. In particular, this theorem states that multiplying a vector by a positive scalar does not change the ray in which the vector lies.
More concisely: Given strict ordered commutative semirings `R` and `S`, an additive commutative `R`-module `M`, vectors `x, y` in `M`, a strictly positive scalar `a` in `S`, if `x` and `y` lie on the same ray, then `x` and `a` times `y` also lie on the same ray.
|
SameRay.of_neg
theorem SameRay.of_neg :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x y : M}, SameRay R (-x) (-y) → SameRay R x y
The theorem `SameRay.of_neg` states that for any strict ordered commutative ring `R`, any additive commutative group `M`, and any module `M` over `R`, if two vectors `-x` and `-y` are in the same ray (in other words, if `-x` and `-y` are either both zero or there exist positive multiples of them that are equal), then the vectors `x` and `y` are also in the same ray.
More concisely: If two vectors `-x` and `-y` lie on the same ray in an additive commutative group `M` over a strict ordered commutative ring `R`, then `x` and `y` also lie on the same ray.
|
Module.Ray.ne_neg_self
theorem Module.Ray.ne_neg_self :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] (x : Module.Ray R M), x ≠ -x
This theorem states that in a module `M` over a strictly ordered commutative ring `R`, where `M` is an additive group and `R` and `M` have no zero `smul` divisors, a ray `x` is not equal to its own negation. This means that for any ray `x` in the module, the negative of `x` is not the same as `x`.
More concisely: In a strictly ordered commutative ring `R` with no zero `smul` divisors, for any non-zero element `x` in the additive group `M` of an `R`-module, `-x ≠ x`.
|
SameRay.add_right
theorem SameRay.add_right :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y z : M}, SameRay R x y → SameRay R x z → SameRay R x (y + z)
This theorem states that if `y` and `z` are on the same ray as `x` in a module over a strict ordered commutative semiring, then so is `y + z`. In other words, within this mathematical structure, if `y` and `z` can be expressed as positive multiples of `x` (or if either `y`, `z` or `x` are zero), then the sum of `y` and `z` is also on the same ray as `x`, meaning it can be expressed as a positive multiple of `x` (or is zero).
More concisely: If `x`, `y`, and `z` are elements in a module over a strict ordered commutative semiring such that `y = mx` and `z = nx` for some `m` and `n` in the semiring, then `y + z = (m + n)x`.
|
sameRay_of_mem_orbit
theorem sameRay_of_mem_orbit :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{v₁ v₂ : M}, v₁ ∈ MulAction.orbit (↥(Units.posSubgroup R)) v₂ → SameRay R v₁ v₂
This theorem states that for any linear ordered commutative ring `R` and any additive commutative group `M` that is also a module over `R`, if a vector `v₁` is in the orbit of vector `v₂` under the action of the positive units (i.e., the multiplicative subgroup of positive elements) of `R`, then `v₁` and `v₂` are in the same ray. In other words, `v₁` and `v₂` are in the same ray if either one of them is zero or some positive multiples of them are equal.
More concisely: For any linear ordered commutative ring `R`, any additive commutative group `M` that is an `R`-module, and vectors `v₁` and `v₂` in `M`, if there exists a positive unit `u` in `R` such that `u * v₁ = v₂`, then `v₁` and `v₂` lie on the same ray.
|
sameRay_smul_right_iff_of_ne
theorem sameRay_smul_right_iff_of_ne :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {v : M}, v ≠ 0 → ∀ {r : R}, r ≠ 0 → (SameRay R v (r • v) ↔ 0 < r)
The theorem, `sameRay_smul_right_iff_of_ne`, states that for a non-zero vector `v` in a module `M` over a linearly ordered commutative ring `R` (where no non-zero scalar multiplied by a vector gives a zero vector), `v` is in the same ray as a scalar multiple `r • v` of itself if and only if that scalar `r` is positive. In other words, a non-zero vector `v` and its scaled version `r • v` are considered to be in the same direction (or "ray") if and only if the scaling factor `r` is greater than zero. This highlights the geometric interpretation of scalar multiplication in vector spaces, where positive scalars do not change the direction of the vector.
More concisely: For a non-zero vector `v` in a module `M` over a linearly ordered commutative ring `R` with no zero-divisors, `v` and `r • v` are in the same ray for any positive `r` in `R`.
|
SameRay.exists_nonneg_right
theorem SameRay.exists_nonneg_right :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x y : M}, SameRay R x y → y ≠ 0 → ∃ r, 0 ≤ r ∧ x = r • y
The theorem `SameRay.exists_nonneg_right` states that for any ordered field `R` and any additive commutative group `M` which is also an `R`-module, if a vector `x` lies on the same ray as a non-zero vector `y` (i.e., `x` and `y` are either both zero or there exist positive scalars such that `x` is a scaled version of `y`), then there exists a non-negative scalar `r` such that `x` can be expressed as `r` times `y`.
More concisely: Given an ordered field `R` and an additive commutative group `M` that is an `R`-module, if `x` and `non-zero y` lie on the same ray in `M`, then there exists a non-negative scalar `r` in `R` such that `x = r * y`.
|
SameRay.refl
theorem SameRay.refl :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (x : M), SameRay R x x
The theorem states that the relation `SameRay` is reflexive. In the context of a strict ordered commutative semiring `R` and an additive commutative monoid `M` that is also an `R`-module, this means that for every vector `x` in `M`, `x` is in the same ray as itself. More intuitively, a vector is always in the same direction as itself, either because the vector is zero, or because any positive multiple of the vector is equal to another positive multiple of the same vector.
More concisely: In the context of a strict ordered commutative semiring R and an additive commutative monoid M that is also an R-module, the relation SameRay on M is reflexive, that is, for all x in M, x ∉ {} ∧ ∃ (n : ℕ), x = n * x.
|
SameRay.map
theorem SameRay.map :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {x y : M} (f : M →ₗ[R] N),
SameRay R x y → SameRay R (f x) (f y)
This theorem states that if two vectors belong to the same ray in a vector space over a strictly ordered commutative semiring, then their images under any linear map also belong to the same ray in the target space. In other words, the relationship of being in the same ray is preserved under linear transformations. The vectors are considered to be in the same ray if either one of them is the zero vector, or they are positive multiples of each other.
More concisely: If two vectors in a vector space over a strictly ordered commutative semiring are in the same ray, then their images under any linear map are also in the same ray in the target space.
|
RayVector.equiv_neg_iff
theorem RayVector.equiv_neg_iff :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{v₁ v₂ : RayVector R M}, -v₁ ≈ -v₂ ↔ v₁ ≈ v₂
The theorem `RayVector.equiv_neg_iff` states that for any strict ordered commutative ring `R` and any type `M` which is an additive commutative group and an `R`-module, if two nonzero vectors `v₁` and `v₂` in `M` are equivalent, then their negations `-v₁` and `-v₂` are also equivalent and vice versa. In other words, the equivalence of two nonzero vectors is preserved under negation.
More concisely: For any strict ordered commutative ring `R`, additive commutative group and `R`-module `M` with two nonzero vectors `v₁` and `v₂`, if `v₁ ≈ v₂`, then `-v₁ ≈ -v₂`.
|
sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent
theorem sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {x y : M},
SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
The theorem `sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent` states that for any type `R` with a linear ordering and commutative ring operations, type `M` with an additive group structure and `M` being a module over `R`, and assuming that there are no zero scalar multiples or divisors in `M`, two vectors `x` and `y` are in the same ray (i.e., one is a nonnegative scalar multiple of the other or one of them is zero), or both `x` and `y` are nonzero and `x` is in the same ray as the negation of `y`, if and only if the pair `x` and `y` is not linearly independent. That is, the vectors `x` and `y` are linearly dependent if and only if they are in the same ray or they are both nonzero and `x` is in the same ray as `-y`.
More concisely: Two vectors in an R-module M with a linear ordering and no zero scalar multiples or divisors are linearly dependent if and only if they are in the same ray or both are nonzero and one is in the same ray as the negation of the other.
|
SameRay.nonneg_smul_right
theorem SameRay.nonneg_smul_right :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {x y : M} {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R]
[inst_5 : Module S M] [inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S},
SameRay R x y → 0 ≤ a → SameRay R x (a • y)
This theorem states that for any vector `x` and `y`, if `x` and `y` are in the same ray (i.e., `x` is either zero, `y` is zero, or there exist positive multiples `r₁` and `r₂` such that `r₁ * x = r₂ * y`), then `x` is also in the same ray as any nonnegative multiple of `y`. Here, the nonnegative multiple of `y` is represented by `a • y`, where `a` is a nonnegative scalar. This holds in the context of a strictly ordered commutative semiring `R`, an additive commutative monoid `M`, and a module structure over `R` and `M`.
More concisely: If `x` and `y` are in the same ray in a commutative semiring with a module structure over an additive commutative monoid, then `x` is in the same ray as any nonnegative scalar multiple of `y`.
|
Module.Ray.units_smul_of_neg
theorem Module.Ray.units_smul_of_neg :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(u : Rˣ), ↑u < 0 → ∀ (v : Module.Ray R M), u • v = -v
This theorem states that in the context of a strictly ordered commutative ring `R` and a module `M` over `R` with an additive commutative group structure, if we have a unit element `u` in `R` which is negative, then scaling any ray `v` in the module `M` by the unit `u` is equivalent to the negation of the ray `v`. In other words, multiplying a ray by a negative unit flips the direction of the ray.
More concisely: In a strictly ordered commutative ring with a unit `u` of negative order, scaling a ray `v` in a module by `u` is equivalent to the negation of `v`.
|
Module.Ray.someVector_ne_zero
theorem Module.Ray.someVector_ne_zero :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (x : Module.Ray R M), x.someVector ≠ 0
This theorem states that for any given module `M` over a strictly ordered commutative semiring `R`, and for any ray `x` in this module, the vector `someVector` associated with this ray is not zero. This encapsulates the mathematical notion that a ray is defined as an equivalence class of nonzero vectors with common positive multiples, hence the representative vector `someVector` cannot be zero.
More concisely: For any module M over a strictly ordered commutative semiring R and any ray x in M, the representative vector someVector of x is nonzero.
|
SameRay.sameRay_nonneg_smul_left
theorem SameRay.sameRay_nonneg_smul_left :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {S : Type u_5} [inst_3 : OrderedCommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M]
[inst_6 : SMulPosMono S R] [inst_7 : IsScalarTower S R M] {a : S} (v : M), 0 ≤ a → SameRay R (a • v) v
The theorem `SameRay.sameRay_nonneg_smul_left` states that for any vector `v` and any nonnegative scalar `a` in a module `M` over a strictly ordered commutative semiring `R`, where `R` is an algebra over another ordered commutative semiring `S`, and where scalar multiplication by positive elements of `S` on `R` is monotonically increasing, and `S`, `R` and `M` form a scalar tower (i.e., scalar multiplication by an element of `S` followed by an element of `R` is the same as scalar multiplication by the product of those elements), then the vector which is the result of scaling `v` by `a`, is in the same ray as `v`. In other words, `a • v` and `v` are considered to be pointing in the same direction, or they are in the same "ray".
More concisely: For any nonnegative scalar `a` in an ordered commutative semiring `S` over a module `M` over a strictly ordered commutative semiring `R`, where scalar multiplication by positive elements of `S` on `R` is monotonic and `S`, `R`, and `M` form a scalar tower, if `v` is a vector in `M`, then `a • v` and `v` lie on the same ray.
|
Module.Ray.someRayVector_ray
theorem Module.Ray.someRayVector_ray :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (x : Module.Ray R M), ⟦x.someRayVector⟧ = x
This theorem, `Module.Ray.someRayVector_ray`, states that for any type `R` that is a strictly ordered commutative semiring, and for any type `M` that is an additive commutative monoid and a module over `R`, for every ray `x` in the module `M`, the equivalence class of the vector associated with the ray `x` is the same as the ray `x` itself. In other words, this theorem is saying that the ray associated with a given vector (obtained through the `someRayVector` function) is essentially the same as the original ray when we consider vectors that are scalar multiples of each other to be equivalent.
More concisely: For any strictly ordered commutative semiring `R`, additive commutative monoid and `R`-module `M`, and ray `x` in `M`, the ray `x` is equivalent to the vector associated with `x` through `someRayVector` function.
|
SameRay.exists_eq_smul
theorem SameRay.exists_eq_smul :
∀ {R : Type u_1} [inst : LinearOrderedField R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{v₁ v₂ : M}, SameRay R v₁ v₂ → ∃ u a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u
The theorem asserts that if two vectors `v₁` and `v₂` are on the same ray in a linearly ordered field `R` over an additive commutative group `M` (which is also a `R`-module), then they are nonnegative multiples of the same vector `u`. This vector `u` can be expressed in terms of `v₁` and `v₂` as `a • v₁` and `b • v₂` where `a` and `b` are nonnegative scalars that add up to 1. This means `v₁` and `v₂` are different scalar multiples of the same vector, which confirms them being on the same ray. Note that this vector `u` can ultimately be assumed to be `v₁ + v₂`, as outlined in `SameRay.exists_eq_smul_add`.
More concisely: If two vectors `v₁` and `v₂` lie on the same ray in a linearly ordered field `R` over an additive commutative group `M` (which is also an `R`-module), then there exist nonnegative scalars `a` and `b` in `R` with `a + b = 1` such that `v₁ = a * u` and `v₂ = b * u` for some vector `u` in `M`.
|
sameRay_neg_iff
theorem sameRay_neg_iff :
∀ {R : Type u_1} [inst : StrictOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{x y : M}, SameRay R (-x) (-y) ↔ SameRay R x y
The theorem `sameRay_neg_iff` states that for any strict ordered commutative ring `R`, and an additive commutative group `M` which is also a module over `R`, any two elements `x` and `y` of `M` are in the same ray if and only if their negations `-x` and `-y` are in the same ray. The concept of being in the "same ray" involves the vectors being zero or the existence of positive multiples of them that are equal (i.e., one vector is a positive scalar multiple of the other).
More concisely: For any strict ordered commutative ring R and additive commutative group M as an R-module, x and y in M are in the same ray if and only if -x and -y are in the same ray.
|
Mathlib.LinearAlgebra.Ray._auxLemma.1
theorem Mathlib.LinearAlgebra.Ray._auxLemma.1 :
∀ {R : Type u_1} [inst : StrictOrderedCommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (y : M), SameRay R 0 y = True
The theorem states that for any strictly ordered commutative semiring `R` and an additive commutative monoid `M` that also is a module over `R`, any vector `y` in `M` lies in the same ray as the zero vector. In other words, the zero vector and any other vector `y` satisfy the property `SameRay`, which is defined to be true when either of the vectors is zero, or when some positive multiples of the vectors are equal.
More concisely: For any strictly ordered commutative semiring R and an additive commutative monoid M that is an R-module, every non-zero vector y in M lies on the same ray as the zero vector.
|
sameRay_smul_left_iff_of_ne
theorem sameRay_smul_left_iff_of_ne :
∀ {R : Type u_1} [inst : LinearOrderedCommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] {v : M}, v ≠ 0 → ∀ {r : R}, r ≠ 0 → (SameRay R (r • v) v ↔ 0 < r)
This theorem states that for any nonzero vector `v` and any nonzero scalar `r` in a given context of a linearly ordered commutative ring, an additive commutative group, and a module where no nonzero elements can result in a zero scalar multiplication or division, the scalar multiple `r • v` lies on the same ray as the vector `v` if and only if `r` is positive. This essentially means that a vector and its positive scalar multiple are always in the same direction.
More concisely: For any nonzero vector `v` and scalar `r` in a linearly ordered commutative ring with no zero-divisors, `r • v` lies on the same ray as `v` if and only if `r` is positive.
|