Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-06 06:05 f811910b

View on Github →

feat(linear_algebra/affine_space/barycentric_coords): barycentric coordinates are 1 in zero dimensions (#9564)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.subsingleton_of_univ_subsingleton

added theorem set.subsingleton_univ_iff

Modified src/linear_algebra/affine_space/affine_subspace.lean

added theorem affine_subspace.subsingleton_of_subsingleton_span_eq_top

Modified src/linear_algebra/affine_space/barycentric_coords.lean

added theorem coe_barycentric_coord_of_subsingleton_eq_one