AffineMap.lineMap_vsub_left
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) c -ᵥ p₀ = c • (p₁ -ᵥ p₀)- Cited by
- 9 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- 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
- VSub.vsubstatement and proof · cited by 817
- AffineMapstatement · cited by 674
- LinearMap.idproof · cited by 625
- AffineMap.lineMapstatement · cited by 254
- vadd_vsubproof · cited by 58
- LinearMap.smulRightproof · cited by 54
- LinearMap.toAffineMapproof · cited by 16
Cited by9
Results whose statement or proof uses this declaration.
- midpoint_vsub_leftproof · cited by 6
- Wbtw.sameRay_vsub_leftproof · cited by 2
- Wbtw.trans_leftproof · cited by 2
- AffineMap.left_vsub_lineMapproof · cited by 2
- AffineIndependent.units_lineMapproof · cited by 1
- affineSpan_eq_affineSpan_lineMap_unitsproof · cited by 1
- AffineMap.lineMap_vsub_rightproof · cited by 0
- EuclideanGeometry.dist_le_of_wbtw_of_mem_perpBisectorproof · cited by 0