Theorems · Theorem · geometry

AffineBasis.basisOf_reindex

∀ {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V]
  [inst_1 : AddTorsor V P] [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i : ι'),
  (b.reindex e).basisOf i = (b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)

Defined in

Mathlib.LinearAlgebra.AffineSpace.Basis

Cited by

1 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupAddTorsorRingModule