Theorems · Definition · geometry

AffineMap.comp

{k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          {V3 : Type u_6} →
            {P3 : Type u_7} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V1] →
                  [inst_2 : Module k V1] →
                    [inst_3 : AddTorsor V1 P1] →
                      [inst_4 : AddCommGroup V2] →
                        [inst_5 : Module k V2] →
                          [inst_6 : AddTorsor V2 P2] →
                            [inst_7 : AddCommGroup V3] →
                              [inst_8 : Module k V3] →
                                [inst_9 : AddTorsor V3 P3] → (P2 →ᵃ[k] P3) → (P1 →ᵃ[k] P2) → P1 →ᵃ[k] P3

Composition of affine maps.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

20 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddTorsorAddCommGroupModuleAddTorsorAddCommGroupModuleAddTorsor