Commit 2022-05-18 20:08 32700f50

View on Github →

refactor(*): insert_singleton → pair (#14210) We rename various theorems with insert_singleton in the name to the more sensible and searchable pair. We also golf finset.pair_comm.

Estimated changes

Modified src/data/finset/basic.lean

deleted theorem finset.insert_singleton_comm

deleted theorem finset.insert_singleton_self_eq

added theorem finset.pair_comm

added theorem finset.pair_self_eq

Modified src/geometry/euclidean/basic.lean

deleted theorem euclidean_geometry.cospherical_insert_singleton

added theorem euclidean_geometry.cospherical_pair

Modified src/geometry/euclidean/circumcenter.lean

Modified src/geometry/euclidean/monge_point.lean

deleted theorem affine.simplex.affine_span_insert_singleton_eq_altitude_iff

added theorem affine.simplex.affine_span_pair_eq_altitude_iff

Modified src/group_theory/perm/support.lean

Modified src/linear_algebra/affine_space/combination.lean

deleted theorem finset.centroid_insert_singleton

deleted theorem finset.centroid_insert_singleton_fin

added theorem finset.centroid_pair

added theorem finset.centroid_pair_fin

Modified src/linear_algebra/affine_space/finite_dimensional.lean

deleted theorem collinear_insert_singleton

added theorem collinear_pair

Modified src/number_theory/divisors.lean