AffineIndependent.injective
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P}, AffineIndependent k p → Function.Injective pAn affinely independent family is injective, if the underlying ring is nontrivial.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Nontrivialstatement and proof · cited by 2,416
- AddTorsorstatement and proof · cited by 1,657
- AffineIndependentstatement and proof · cited by 144
- vsub_eq_zero_iff_eqproof · cited by 45
- LinearIndependent.ne_zeroproof · cited by 20
- affineIndependent_iff_linearIndependent_vsubproof · cited by 11
Cited by21
Results whose statement or proof uses this declaration.
- Affine.Simplex.ExcenterExists.touchpoint_injectiveproof · cited by 4
- AffineIndependent.finrank_vectorSpan_image_finsetproof · cited by 3
- Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradiusproof · cited by 2
- EuclideanGeometry.exists_of_range_subset_orthocentricSystemproof · cited by 2
- Affine.Simplex.centroid_eq_of_range_eqproof · cited by 2
- Affine.Triangle.touchpoint_singleton_sbtwproof · cited by 2
- Affine.Simplex.circumradius_posproof · cited by 1
- Affine.Triangle.altitude_replace_orthocenter_eq_affineSpanproof · cited by 1
- Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradiusproof · cited by 1
- Polygon.HasNondegenerateVertices.hasNondegenerateEdgesproof · cited by 1
- Affine.Simplex.mem_interior_iff_sbtwproof · cited by 1