Theorems · Theorem · linear algebra
SameRay.congr_simp
∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
[inst_3 : AddCommMonoid M] [inst_4 : Module R M] (v₁ v₁_1 : M),
v₁ = v₁_1 → ∀ (v₂ v₂_1 : M), v₂ = v₂_1 → SameRay R v₁ v₂ = SameRay R v₁_1 v₂_1- Defined in
- Mathlib.LinearAlgebra.Ray
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- PartialOrderstatement and proof · cited by 6,410
- IsStrictOrderedRingstatement and proof · cited by 2,490
- SameRaystatement and proof · cited by 149
Cited by18
Results whose statement or proof uses this declaration.
- Wbtw.wOppSide₁₃proof · cited by 4
- Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eqproof · cited by 3
- Wbtw.sameRay_vsub_leftproof · cited by 2
- Function.Injective.wOppSide_map_iffproof · cited by 2
- Function.Injective.wSameSide_map_iffproof · cited by 2
- sameRay_of_mem_segmentproof · cited by 2
- sameRay_or_sameRay_neg_iff_not_linearIndependentproof · cited by 2
- Wbtw.sameRay_vsubproof · cited by 1
- StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticConeproof · cited by 1
- isConnected_setOfPred_sameRayproof · cited by 1
- Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRayproof · cited by 1
- AffineSubspace.WOppSide.mapproof · cited by 1