AffineMap.lineMap_same
∀ {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 : P1), AffineMap.lineMap p p = AffineMap.const k k p- Cited by
- 13 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, 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
- AddTorsorstatement and proof · cited by 1,657
- AffineMapstatement · cited by 674
- AffineMap.lineMapstatement · cited by 254
- AffineMap.extproof · cited by 19
- AffineMap.conststatement · cited by 14
- AffineMap.lineMap_same_applyproof · cited by 5
Cited by13
Results whose statement or proof uses this declaration.
- wbtw_self_iffproof · cited by 4
- wbtw_iff_left_eq_or_right_mem_image_Iciproof · cited by 4
- Path.segment_sameproof · cited by 2
- List.exists_map_eq_of_sorted_nonempty_iff_wbtwproof · cited by 2
- Circle.path_selfproof · cited by 2
- lineMap_slope_lineMap_slope_lineMapproof · cited by 1
- AffineIndependent.units_lineMapproof · cited by 1
- EuclideanGeometry.Sphere.dist_center_lt_radius_of_sbtwproof · cited by 1
- affineSpan_eq_affineSpan_lineMap_unitsproof · cited by 1
- IsClosed.exists_wbtw_isVisibleproof · cited by 1
- eq_lineMap_of_dist_eq_mul_of_dist_eq_mulproof · cited by 1
- affineSegment_sameproof · cited by 0