Theorems · Definition · geometry

AffineEquiv.pointReflection

(k : Type u_1) →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → P₁ → P₁ ≃ᵃ[k] P₁

The affine equivalence given by reflection about the point x. This is Equiv.pointReflection as an AffineEquiv.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Cited by

32 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor