Affine.Simplex.independent
∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {n : ℕ} (self : Affine.Simplex k P n), AffineIndependent k self.points- Cited by
- 45 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- AddTorsorstatement and proof · cited by 1,657
- Affine.Simplexstatement and proof · cited by 471
- Affine.Simplex.pointsstatement · cited by 391
- AffineIndependentstatement · cited by 144
Cited by45
Results whose statement or proof uses this declaration.
- Affine.Simplex.circumsphere_unique_dist_eqproof · cited by 6
- Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iffproof · cited by 6
- Affine.Simplex.affineCombination_mem_setInterior_iffproof · cited by 5
- Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceproof · cited by 4
- Affine.Simplex.ExcenterExists.touchpoint_injectiveproof · cited by 4
- EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subsetproof · cited by 3
- EuclideanGeometry.exists_circumradius_eq_of_cospherical_subsetproof · cited by 3
- Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eqproof · cited by 3
- Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_negproof · cited by 3
- Affine.Simplex.affineCombination_eq_touchpoint_iffproof · cited by 3
- Affine.Simplex.touchpointWeights_eq_zeroproof · cited by 3
- Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradiusproof · cited by 2