Mathlib Map

Theorems · Definition · geometry

AffineMap.id

(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] → P1 →ᵃ[k] P1

Identity map as an affine map.

Defined in
Mathlib.LinearAlgebra.AffineSpace.AffineMap
Cited by
16 results in Mathlib
Foundations
Depth 22 from the axioms · uses no axioms
Assumes
RingAddCommGroupModuleAddTorsor
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AffineMap.homothety · cited by 51AffineMap.homothetyAffineIsometry.id · cited by 6AffineIsometry.idContinuousAffineMap.id · cited by 5ContinuousAffineMap.idAffineSubspace.map_id · cited by 3AffineSubspace.map_idAffineMap.homothety_one · cited by 3AffineMap.homothety_oneconvexOn_dist · cited by 2convexOn_distConvexOn.strictAntiOn · cited by 2ConvexOn.strictAntiOnAffineMap.homothetyAffine · cited by 1AffineMap.homothetyAffineAffineEquiv.coe_refl_to_affineMap · cited by 1AffineEquiv.coe_refl_to_a…AffineMap.homothety_add · cited by 0AffineMap.homothety_addAffineMap.homothety_def · cited by 0AffineMap.homothety_defAffineMap.coe_id · cited by 0AffineMap.coe_idAffineSubspace.inclusion_rfl · cited by 0AffineSubspace.inclusion_…AffineSubspace.comap_id · cited by 0AffineSubspace.comap_idAffineMap.id_apply · cited by 0AffineMap.id_applyModule · cited by 20661ModuleAddCommGroup · cited by 12871AddCommGroupRing · cited by 7463RingAddTorsor · cited by 1657AddTorsorAffineMap · cited by 674AffineMapLinearMap.id · cited by 625LinearMap.idAffineMap.idCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by20

Results whose statement or proof uses this declaration.