hoskinson-center/proofnet

1-- basic mathematics2import algebra.group.pi3import algebra.group.commute4import algebra.group_power.basic5import algebra.group_power.identities6import analysis.inner_product_space.basic7import analysis.inner_product_space.euclidean_dist8import analysis.special_functions.exp9import analysis.special_functions.exp_deriv10import analysis.special_functions.log.base11import analysis.special_functions.log.basic12import analysis.special_functions.log.deriv13import analysis.special_functions.log.monotone14import analysis.special_functions.pow15import analysis.special_functions.sqrt16import analysis.special_functions.trigonometric.basic17import analysis.special_functions.trigonometric.complex18import data.fintype.card19import data.int.parity20import data.list.intervals21import data.nat.factorial.basic22import data.nat.multiplicity23import data.set.finite24import data.sym.sym225import logic.equiv.basic26import number_theory.legendre_symbol.quadratic_reciprocity27import number_theory.primes_congruent_one28import order.well_founded29import algebra.algebra.basic30import algebra.big_operators31import algebra.big_operators.basic32import algebra.big_operators.order33import algebra.big_operators.pi34import algebra.associated35import algebra.order.floor36import algebra.geom_sum37import algebra.quadratic_discriminant38import algebra.ring.basic39import analysis.asymptotics.asymptotic_equivalent40import analysis.mean_inequalities41import analysis.normed_space.basic42import analysis.normed_space.pi_Lp43import combinatorics.simple_graph.basic44import data.complex.basic45import data.complex.exponential46import data.is_R_or_C.basic 47import data.finset.basic48import data.finset.lattice49import data.finset.sort50import data.fintype.basic51import data.int.basic52import data.int.gcd53import data.int.modeq54import data.list.basic55import data.list.defs56import data.list.palindrome57import data.matrix.basic58import data.multiset.basic59import data.nat.basic60import data.nat.choose61import data.nat.choose.basic62import data.nat.digits63import data.nat.dist64import data.nat.fib65import data.nat.log66import data.nat.modeq67import data.nat.parity68import data.nat.prime69import data.pnat.basic70import data.pnat.prime71import data.polynomial72import data.polynomial.basic73import data.polynomial.degree.definitions74import data.polynomial.div75import data.polynomial.eval76import data.polynomial.ring_division77import data.rat.basic78import data.real.basic79import data.real.ennreal80import data.real.golden_ratio81import data.real.irrational82import data.real.nnreal83import data.real.pi.bounds84import data.real.pi.leibniz85import data.real.pi.wallis86import data.real.sqrt87import data.set.basic88import data.set.intervals.basic89import data.zmod.basic90import data.fintype.basic91import geometry.euclidean.basic92import geometry.euclidean.circumcenter93import geometry.euclidean.monge_point94import geometry.euclidean.sphere95import init.data.nat.gcd96import linear_algebra.affine_space.affine_map97import linear_algebra.affine_space.independent98import linear_algebra.affine_space.ordered99import linear_algebra.finite_dimensional100import logic.basic101import number_theory.arithmetic_function102import number_theory.divisors103import order.filter.basic104import order.well_founded_set105import set_theory.lists106 107--analysis 108import analysis.calculus.fderiv109import analysis.calculus.cont_diff110import analysis.calculus.iterated_deriv111import dynamics.ergodic.measure_preserving112import measure_theory.integral.interval_integral113 114-- algebra115import algebra.group.basic116import group_theory.order_of_element117import data.real.basic 118import data.fintype.basic119import data.zmod.basic 120import data.countable.basic121import data.set.countable122import group_theory.abelianization123import group_theory.subgroup.basic124import group_theory.quotient_group125import group_theory.index 126import group_theory.specific_groups.cyclic127import group_theory.specific_groups.dihedral128import group_theory.solvable 129import group_theory.free_group130import group_theory.presented_group131import group_theory.group_action.conj_act132import group_theory.sylow133import group_theory.coset 134import number_theory.zsqrtd.gaussian_int135import ring_theory.ideal.operations136import ring_theory.ideal.minimal_prime137import algebra.char_p.basic138import algebra.quaternion139import algebra.gcd_monoid.basic140import algebra.monoid_algebra.basic141import linear_algebra.general_linear_group142import field_theory.finite.galois_field143import deprecated.subgroup144 145-- linear algebra146import linear_algebra.eigenspace147import analysis.inner_product_space.projection148import analysis.inner_product_space.adjoint149 150-- topology151import topology.basic152import topology.constructions153import topology.bases154import topology.stone_cech155import topology.path_connected156import topology.metric_space.metrizable157import topology.algebra.infinite_sum158import topology.instances.nnreal159import topology.metric_space.basic160 161-- number theory 162import number_theory.arithmetic_function163 164