6 src/analysis/bounded_variation.lean 4 src/analysis/constant_speed.lean 2 src/analysis/convex/basic.lean 10 src/analysis/convex/between.lean 1 src/analysis/convex/body.lean 1 src/analysis/convex/caratheodory.lean 3 src/analysis/convex/combination.lean 1 src/analysis/convex/contractible.lean 1 src/analysis/convex/extrema.lean 3 src/analysis/convex/extreme.lean 2 src/analysis/convex/function.lean 8 src/analysis/convex/gauge.lean 3 src/analysis/convex/hull.lean 3 src/analysis/convex/independent.lean 3 src/analysis/convex/integral.lean 5 src/analysis/convex/intrinsic.lean 2 src/analysis/convex/krein_milman.lean 1 src/analysis/convex/measure.lean 17 src/analysis/convex/side.lean 2 src/analysis/convex/slope.lean 1 src/analysis/convex/star.lean 1 src/analysis/convex/stone_separation.lean 1 src/analysis/convex/strict.lean 1 src/analysis/convex/strict_convex_between.lean 6 src/analysis/convex/strict_convex_space.lean 4 src/analysis/convex/topology.lean 1 src/analysis/convex/uniform.lean 11 src/analysis/convolution.lean 1 src/analysis/inner_product_space/adjoint.lean 20 src/analysis/inner_product_space/basic.lean 2 src/analysis/inner_product_space/calculus.lean 4 src/analysis/inner_product_space/dual.lean 2 src/analysis/inner_product_space/euclidean_dist.lean 6 src/analysis/inner_product_space/gram_schmidt_ortho.lean 9 src/analysis/inner_product_space/l2_space.lean 2 src/analysis/inner_product_space/lax_milgram.lean 3 src/analysis/inner_product_space/orientation.lean 2 src/analysis/inner_product_space/orthogonal.lean 10 src/analysis/inner_product_space/pi_L2.lean 1 src/analysis/inner_product_space/positive.lean 3 src/analysis/inner_product_space/rayleigh.lean 7 src/analysis/inner_product_space/spectrum.lean 1 src/analysis/inner_product_space/symmetric.lean 5 src/analysis/inner_product_space/two_dim.lean 1 src/analysis/locally_convex/polar.lean 4 src/analysis/matrix.lean 6 src/analysis/mean_inequalities.lean 3 src/analysis/mean_inequalities_pow.lean 4 src/analysis/p_series.lean 1 src/analysis/quaternion.lean 5 src/analysis/schwartz_space.lean 12 src/analysis/seminorm.lean 2 src/analysis/special_functions/arsinh.lean 3 src/analysis/special_functions/bernstein.lean 4 src/analysis/special_functions/complex/arg.lean 3 src/analysis/special_functions/complex/log.lean 3 src/analysis/special_functions/exp.lean 10 src/analysis/special_functions/gaussian.lean 3 src/analysis/special_functions/improper_integrals.lean 12 src/analysis/special_functions/integrals.lean 5 src/analysis/special_functions/japanese_bracket.lean 5 src/analysis/special_functions/log/basic.lean 4 src/analysis/special_functions/log/deriv.lean 1 src/analysis/special_functions/log/monotone.lean 2 src/analysis/special_functions/non_integrable.lean 2 src/analysis/special_functions/polar_coord.lean 2 src/analysis/special_functions/polynomials.lean 25 src/analysis/special_functions/pow.lean 3 src/analysis/special_functions/pow_deriv.lean 4 src/analysis/special_functions/trigonometric/arctan.lean 1 src/analysis/special_functions/trigonometric/arctan_deriv.lean 1 src/analysis/special_functions/trigonometric/bounds.lean 5 src/analysis/special_functions/trigonometric/chebyshev.lean 2 src/analysis/special_functions/trigonometric/series.lean 2 src/analysis/sum_integral_comparisons.lean 2 src/data/W/cardinal.lean 1 src/data/analysis/filter.lean 4 src/data/array/lemmas.lean 2 src/data/bitvec/basic.lean 1 src/data/bitvec/core.lean 3 src/data/bool/all_any.lean 1 src/data/bool/count.lean 5 src/data/buffer/basic.lean 23 src/data/buffer/parser/basic.lean 1 src/data/char.lean 2 src/data/complex/basic.lean 3 src/data/complex/cardinality.lean 2 src/data/complex/determinant.lean 26 src/data/complex/exponential.lean 3 src/data/complex/module.lean 7 src/data/dfinsupp/basic.lean 3 src/data/dfinsupp/interval.lean 2 src/data/dfinsupp/lex.lean 1 src/data/dfinsupp/multiset.lean 2 src/data/dfinsupp/ne_locus.lean 2 src/data/dfinsupp/order.lean 4 src/data/dfinsupp/well_founded.lean 1 src/data/erased.lean 11 src/data/fin/basic.lean 9 src/data/fin/interval.lean 5 src/data/fin/tuple/basic.lean 1 src/data/fin/tuple/bubble_sort_induction.lean 3 src/data/fin/tuple/nat_antidiagonal.lean 2 src/data/fin/tuple/reflection.lean 4 src/data/fin/tuple/sort.lean 5 src/data/fin/vec_notation.lean 1 src/data/fin_enum.lean 1 src/data/finite/card.lean 18 src/data/finmap.lean 26 src/data/finset/basic.lean 2 src/data/finset/card.lean 4 src/data/finset/fold.lean 2 src/data/finset/functor.lean 7 src/data/finset/image.lean 1 src/data/finset/interval.lean 11 src/data/finset/lattice.lean 13 src/data/finset/locally_finite.lean 1 src/data/finset/mul_antidiagonal.lean 12 src/data/finset/n_ary.lean 1 src/data/finset/nat_antidiagonal.lean 8 src/data/finset/noncomm_prod.lean 2 src/data/finset/option.lean 1 src/data/finset/pi_induction.lean 2 src/data/finset/pimage.lean 9 src/data/finset/pointwise.lean 4 src/data/finset/powerset.lean 1 src/data/finset/preimage.lean 3 src/data/finset/prod.lean 1 src/data/finset/slice.lean 4 src/data/finset/sort.lean 1 src/data/finset/sups.lean 4 src/data/finset/sym.lean 1 src/data/finsupp/alist.lean 2 src/data/finsupp/basic.lean 2 src/data/finsupp/big_operators.lean 10 src/data/finsupp/defs.lean 1 src/data/finsupp/indicator.lean 2 src/data/finsupp/interval.lean 2 src/data/finsupp/multiset.lean 1 src/data/finsupp/ne_locus.lean 2 src/data/finsupp/order.lean 1 src/data/finsupp/pointwise.lean 1 src/data/finsupp/to_dfinsupp.lean 3 src/data/fintype/basic.lean 1 src/data/fintype/big_operators.lean 6 src/data/fintype/card.lean 1 src/data/fintype/card_embedding.lean 2 src/data/fintype/perm.lean 1 src/data/fintype/powerset.lean 1 src/data/fintype/prod.lean 4 src/data/fintype/sum.lean 1 src/data/fintype/units.lean 3 src/data/hash_map.lean 3 src/data/holor.lean 3 src/data/int/basic.lean 3 src/data/int/bitwise.lean 1 src/data/int/cast/lemmas.lean 1 src/data/int/char_zero.lean 9 src/data/int/gcd.lean 2 src/data/int/interval.lean 3 src/data/int/lemmas.lean 3 src/data/int/log.lean 1 src/data/int/modeq.lean 6 src/data/int/order/basic.lean 1 src/data/int/order/lemmas.lean 6 src/data/int/parity.lean 1 src/data/int/sqrt.lean 9 src/data/is_R_or_C/basic.lean 2 src/data/lazy_list/basic.lean 4 src/data/list/alist.lean 36 src/data/list/basic.lean 4 src/data/list/big_operators/basic.lean 3 src/data/list/big_operators/lemmas.lean 4 src/data/list/chain.lean 6 src/data/list/count.lean 6 src/data/list/cycle.lean 2 src/data/list/dedup.lean 1 src/data/list/destutter.lean 2 src/data/list/duplicate.lean 1 src/data/list/fin_range.lean 4 src/data/list/forall2.lean 2 src/data/list/func.lean 9 src/data/list/indexes.lean 6 src/data/list/infix.lean 1 src/data/list/intervals.lean 3 src/data/list/join.lean 3 src/data/list/lattice.lean 7 src/data/list/min_max.lean 1 src/data/list/nat_antidiagonal.lean 1 src/data/list/nodup.lean 1 src/data/list/nodup_equiv_fin.lean 4 src/data/list/of_fn.lean 2 src/data/list/pairwise.lean 1 src/data/list/palindrome.lean 17 src/data/list/perm.lean 4 src/data/list/permutation.lean 4 src/data/list/range.lean 5 src/data/list/rdrop.lean 7 src/data/list/rotate.lean 7 src/data/list/sigma.lean 5 src/data/list/sublists.lean 1 src/data/list/tfae.lean 2 src/data/list/to_finsupp.lean 2 src/data/list/zip.lean 6 src/data/matrix/basic.lean 5 src/data/matrix/block.lean 1 src/data/matrix/notation.lean 4 src/data/matrix/pequiv.lean 5 src/data/matrix/rank.lean 2 src/data/matrix/reflection.lean 1 src/data/multiset/antidiagonal.lean 16 src/data/multiset/basic.lean 1 src/data/multiset/bind.lean 2 src/data/multiset/finset_ops.lean 5 src/data/multiset/fintype.lean 1 src/data/multiset/lattice.lean 9 src/data/multiset/locally_finite.lean 1 src/data/multiset/nat_antidiagonal.lean 1 src/data/multiset/pi.lean 9 src/data/multiset/powerset.lean 1 src/data/multiset/sections.lean 6 src/data/mv_polynomial/basic.lean 1 src/data/mv_polynomial/comap.lean 3 src/data/mv_polynomial/comm_ring.lean 4 src/data/mv_polynomial/equiv.lean 1 src/data/mv_polynomial/funext.lean 5 src/data/mv_polynomial/monad.lean 1 src/data/mv_polynomial/pderiv.lean 1 src/data/mv_polynomial/polynomial.lean 3 src/data/mv_polynomial/supported.lean 7 src/data/mv_polynomial/variables.lean 5 src/data/nat/basic.lean 3 src/data/nat/bits.lean 2 src/data/nat/bitwise.lean 1 src/data/nat/cast/basic.lean 1 src/data/nat/cast/field.lean 1 src/data/nat/choose/basic.lean 1 src/data/nat/choose/cast.lean 2 src/data/nat/choose/central.lean 1 src/data/nat/choose/dvd.lean 2 src/data/nat/choose/factorization.lean 2 src/data/nat/choose/multinomial.lean 3 src/data/nat/choose/sum.lean 1 src/data/nat/count.lean 9 src/data/nat/digits.lean 2 src/data/nat/dist.lean 3 src/data/nat/factorial/basic.lean 2 src/data/nat/factorial/cast.lean 11 src/data/nat/factorization/basic.lean 4 src/data/nat/factorization/prime_pow.lean 3 src/data/nat/factors.lean 6 src/data/nat/fib.lean 9 src/data/nat/gcd/basic.lean 5 src/data/nat/interval.lean 3 src/data/nat/lattice.lean 5 src/data/nat/log.lean 5 src/data/nat/modeq.lean 8 src/data/nat/multiplicity.lean 7 src/data/nat/nth.lean 8 src/data/nat/order/basic.lean 1 src/data/nat/order/lemmas.lean 1 src/data/nat/pairing.lean 5 src/data/nat/parity.lean 7 src/data/nat/part_enat.lean 1 src/data/nat/periodic.lean 5 src/data/nat/pow.lean 1 src/data/nat/prime.lean 2 src/data/nat/prime_fin.lean 1 src/data/nat/size.lean 2 src/data/nat/sqrt.lean 5 src/data/nat/squarefree.lean 5 src/data/nat/totient.lean 1 src/data/nat/upto.lean 1 src/data/nat/with_bot.lean 26 src/data/num/lemmas.lean 1 src/data/num/prime.lean 2 src/data/option/basic.lean 19 src/data/ordmap/ordset.lean 2 src/data/part.lean 2 src/data/pequiv.lean 8 src/data/pfun.lean 4 src/data/pfunctor/multivariate/M.lean 2 src/data/pfunctor/multivariate/W.lean 7 src/data/pfunctor/univariate/M.lean 1 src/data/pfunctor/univariate/basic.lean 1 src/data/pi/algebra.lean 3 src/data/pi/lex.lean 3 src/data/pnat/basic.lean 6 src/data/pnat/factors.lean 1 src/data/pnat/find.lean 5 src/data/pnat/interval.lean 4 src/data/pnat/prime.lean 7 src/data/pnat/xgcd.lean 2 src/data/polynomial/algebra_map.lean 14 src/data/polynomial/basic.lean 4 src/data/polynomial/coeff.lean 1 src/data/polynomial/degree/card_pow_degree.lean 18 src/data/polynomial/degree/definitions.lean 6 src/data/polynomial/degree/lemmas.lean 3 src/data/polynomial/degree/trailing_degree.lean 10 src/data/polynomial/derivative.lean 3 src/data/polynomial/div.lean 2 src/data/polynomial/erase_lead.lean 6 src/data/polynomial/eval.lean 2 src/data/polynomial/expand.lean 12 src/data/polynomial/field_division.lean 3 src/data/polynomial/hasse_deriv.lean 1 src/data/polynomial/identities.lean 1 src/data/polynomial/induction.lean 7 src/data/polynomial/laurent.lean 3 src/data/polynomial/lifts.lean 3 src/data/polynomial/mirror.lean 2 src/data/polynomial/module.lean 7 src/data/polynomial/monic.lean 1 src/data/polynomial/partial_fractions.lean 5 src/data/polynomial/reverse.lean 15 src/data/polynomial/ring_division.lean 6 src/data/polynomial/splits.lean 2 src/data/polynomial/taylor.lean 8 src/data/polynomial/unit_trinomial.lean 1 src/data/prod/basic.lean 3 src/data/prod/tprod.lean 1 src/data/qpf/multivariate/basic.lean 3 src/data/qpf/multivariate/constructions/cofix.lean 3 src/data/qpf/multivariate/constructions/fix.lean 5 src/data/qpf/univariate/basic.lean 4 src/data/rat/cast.lean 3 src/data/rat/defs.lean 4 src/data/rat/floor.lean 6 src/data/rat/lemmas.lean 5 src/data/rat/nnrat.lean 3 src/data/rat/order.lean 1 src/data/rat/sqrt.lean 5 src/data/rbmap/default.lean 1 src/data/rbtree/basic.lean 12 src/data/rbtree/insert.lean 10 src/data/rbtree/main.lean 8 src/data/real/basic.lean 6 src/data/real/cardinality.lean 7 src/data/real/cau_seq.lean 5 src/data/real/cau_seq_completion.lean 17 src/data/real/ennreal.lean 9 src/data/real/ereal.lean 2 src/data/real/golden_ratio.lean 14 src/data/real/hyperreal.lean 2 src/data/real/irrational.lean 3 src/data/real/nnreal.lean 3 src/data/real/pi/bounds.lean 1 src/data/real/pi/leibniz.lean 5 src/data/real/pointwise.lean 2 src/data/real/sign.lean 4 src/data/real/sqrt.lean 3 src/data/rel.lean 3 src/data/semiquot.lean 5 src/data/seq/computation.lean 1 src/data/seq/parallel.lean 5 src/data/seq/seq.lean 11 src/data/seq/wseq.lean 1 src/data/set/accumulate.lean 5 src/data/set/basic.lean 4 src/data/set/countable.lean 13 src/data/set/finite.lean 8 src/data/set/function.lean 7 src/data/set/image.lean 10 src/data/set/intervals/basic.lean 2 src/data/set/intervals/disjoint.lean 5 src/data/set/intervals/group.lean 1 src/data/set/intervals/monoid.lean 1 src/data/set/intervals/monotone.lean 4 src/data/set/intervals/ord_connected.lean 3 src/data/set/intervals/ord_connected_component.lean 1 src/data/set/intervals/pi.lean 3 src/data/set/intervals/surj_on.lean 1 src/data/set/intervals/unordered_interval.lean 8 src/data/set/intervals/with_bot_top.lean 17 src/data/set/lattice.lean 1 src/data/set/list.lean 1 src/data/set/mul_antidiagonal.lean 1 src/data/set/n_ary.lean 1 src/data/set/opposite.lean 2 src/data/set/pairwise/basic.lean 1 src/data/set/pairwise/lattice.lean 6 src/data/set/pointwise/basic.lean 1 src/data/set/pointwise/big_operators.lean 7 src/data/set/pointwise/interval.lean 1 src/data/set/pointwise/list_of_fn.lean 6 src/data/set/prod.lean 2 src/data/set/sigma.lean 1 src/data/set/sups.lean 2 src/data/setoid/basic.lean 2 src/data/setoid/partition.lean 1 src/data/sigma/order.lean 2 src/data/sign.lean 12 src/data/stream/init.lean 4 src/data/string/basic.lean 4 src/data/sum/basic.lean 4 src/data/sym/basic.lean 4 src/data/sym/card.lean 4 src/data/sym/sym2.lean 1 src/data/tree.lean 2 src/data/typevec.lean 10 src/data/vector/basic.lean 1 src/data/vector/mem.lean 1 src/data/vector/zip.lean 2 src/data/vector3.lean 10 src/data/zmod/basic.lean 3 src/data/zmod/quotient.lean 2 src/model_theory/basic.lean 5 src/model_theory/definability.lean 2 src/model_theory/direct_limit.lean 2 src/model_theory/elementary_maps.lean 1 src/model_theory/encoding.lean 1 src/model_theory/finitely_generated.lean 4 src/model_theory/fraisse.lean 1 src/model_theory/language_map.lean 2 src/model_theory/order.lean 1 src/model_theory/quotients.lean 7 src/model_theory/satisfiability.lean 16 src/model_theory/semantics.lean 3 src/model_theory/skolem.lean 4 src/model_theory/substructures.lean 4 src/model_theory/syntax.lean 4 src/model_theory/types.lean 19 src/set_theory/cardinal/basic.lean 16 src/set_theory/cardinal/cofinality.lean 2 src/set_theory/cardinal/divisibility.lean 3 src/set_theory/cardinal/finite.lean 15 src/set_theory/cardinal/ordinal.lean 3 src/set_theory/game/basic.lean 3 src/set_theory/game/domineering.lean 3 src/set_theory/game/impartial.lean 4 src/set_theory/game/nim.lean 1 src/set_theory/game/ordinal.lean 6 src/set_theory/game/pgame.lean 1 src/set_theory/game/short.lean 3 src/set_theory/lists.lean 25 src/set_theory/ordinal/arithmetic.lean 8 src/set_theory/ordinal/basic.lean 3 src/set_theory/ordinal/cantor_normal_form.lean 6 src/set_theory/ordinal/exponential.lean 12 src/set_theory/ordinal/fixed_point.lean 3 src/set_theory/ordinal/natural_ops.lean 12 src/set_theory/ordinal/notation.lean 6 src/set_theory/ordinal/principal.lean 1 src/set_theory/ordinal/topology.lean 2 src/set_theory/surreal/basic.lean 6 src/set_theory/surreal/dyadic.lean 17 src/set_theory/zfc/basic.lean 2 src/set_theory/zfc/ordinal.lean