Commit 2023-04-22 09:23 2d65666a

View on Github →

feat: port LinearAlgebra.AffineSpace.Basis (#3578)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Basis.lean

added theorem AffineBasis.affineCombination_coord_eq_self

added theorem AffineBasis.basisOf_apply

added theorem AffineBasis.basisOf_reindex

added theorem AffineBasis.coe_coord_of_subsingleton_eq_one

added theorem AffineBasis.coe_reindex

added theorem AffineBasis.coord_apply

added theorem AffineBasis.coord_apply_centroid

added theorem AffineBasis.coord_apply_combination_of_mem

added theorem AffineBasis.coord_apply_combination_of_not_mem

added theorem AffineBasis.coord_apply_eq

added theorem AffineBasis.coord_apply_ne

added theorem AffineBasis.coord_reindex

added theorem AffineBasis.coords_apply

added theorem AffineBasis.exists_affineBasis

added theorem AffineBasis.exists_affine_subbasis

added theorem AffineBasis.ext

added theorem AffineBasis.ext_elem

added theorem AffineBasis.ind

added theorem AffineBasis.linear_combination_coord_eq_self

added theorem AffineBasis.linear_eq_sumCoords

added def AffineBasis.reindex

added theorem AffineBasis.reindex_apply

added theorem AffineBasis.reindex_refl

added theorem AffineBasis.sum_coord_apply_eq_one

added theorem AffineBasis.surjective_coord

added theorem AffineBasis.tot

added structure AffineBasis