Commit 2022-04-11 02:03 6f9cb03e

View on Github →

chore(*): make more transitive relations available to calc (#12860) Fixed as many possible declarations to have the correct argument order, as per Zulip. Golfed some random ones while I was at it.

Estimated changes

Modified src/algebra/divisibility.lean

modified theorem dvd_trans

Modified src/analysis/asymptotics/asymptotic_equivalent.lean

modified theorem asymptotics.is_equivalent.trans

modified def asymptotics.is_equivalent

Modified src/analysis/convex/extreme.lean

Modified src/analysis/special_functions/polynomials.lean

Modified src/combinatorics/colex.lean

modified theorem colex.le_trans

modified theorem colex.lt_trans

Modified src/computability/tm_computable.lean

modified def turing.evals_to_in_time.trans

Modified src/computability/turing_machine.lean

Modified src/data/list/rotate.lean

modified theorem list.is_rotated.trans

Modified src/data/set/basic.lean

modified theorem set.mem_of_mem_of_subset

modified theorem set.subset.trans

Modified src/data/sym/sym2.lean

modified theorem sym2.rel.trans

Modified src/logic/equiv/basic.lean

Modified src/measure_theory/integral/interval_integral.lean

modified theorem interval_integrable.trans

Modified src/measure_theory/measure/vector_measure.lean

modified theorem measure_theory.vector_measure.absolutely_continuous.trans

Modified src/order/filter/basic.lean

modified theorem filter.eventually_eq.trans

Modified src/order/ideal.lean

modified theorem order.ideal.mem_of_mem_of_le

Modified src/order/rel_classes.lean

modified theorem ssubset_trans

modified theorem subset_trans

Created test/calc.lean