Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 07:48 00d450eb

View on Github →

refactor(data/set/pairwise): use {{..}} arguments (#17230)

Estimated changes

Modified archive/100-theorems-list/82_cubing_a_cube.lean

Modified src/algebra/big_operators/finprod.lean

Modified src/algebra/direct_sum/module.lean

Modified src/algebra/group/pi.lean

Modified src/data/finset/basic.lean

Modified src/data/mv_polynomial/variables.lean

Modified src/data/polynomial/ring_division.lean

Modified src/data/set/pairwise.lean

modified theorem pairwise.set_pairwise

modified def pairwise

modified theorem pairwise_subtype_iff_pairwise_set

Modified src/field_theory/separable.lean

Modified src/group_theory/free_product.lean

Modified src/group_theory/noncomm_pi_coprod.lean

Modified src/linear_algebra/bilinear_form.lean

Modified src/linear_algebra/quadratic_form/basic.lean

Modified src/linear_algebra/sesquilinear_form.lean

Modified src/logic/encodable/lattice.lean

Modified src/measure_theory/constructions/prod.lean

Modified src/measure_theory/decomposition/lebesgue.lean

Modified src/measure_theory/decomposition/signed_hahn.lean

Modified src/measure_theory/function/jacobian.lean

Modified src/measure_theory/group/fundamental_domain.lean

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/measure/ae_disjoint.lean

Modified src/measure_theory/measure/measure_space.lean

Modified src/measure_theory/measure/outer_measure.lean

Modified src/measure_theory/measure/regular.lean

Modified src/measure_theory/measure/vector_measure.lean

Modified src/measure_theory/pi_system.lean

Modified src/order/disjointed.lean

Modified src/order/filter/basic.lean

Modified src/order/partial_sups.lean

Modified src/order/sup_indep.lean

Modified src/probability/strong_law.lean

Modified src/ring_theory/coprime/lemmas.lean

Modified src/topology/uniform_space/separation.lean

Modified src/topology/uniform_space/uniform_embedding.lean